package rocq-runtime
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
  The Rocq Prover -- Core Binaries and Tools
Install
    
    dune-project
 Dependency
Authors
Maintainers
Sources
  
    
      rocq-9.1.0.tar.gz
    
    
        
    
  
  
  
    
  
        sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824
    
    
  doc/ring_plugin/Ring_plugin/Ring/index.html
Module Ring_plugin.RingSource
Source
val add_theory : 
  Names.Id.t ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr Ring_ast.ring_mod list ->
  unitSource
val ring_lookup : 
  Geninterp.Val.t ->
  EConstr.constr list ->
  EConstr.constr list ->
  EConstr.constr ->
  unit Proofview.tacticSource
val add_field_theory : 
  Names.Id.t ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr Ring_ast.field_mod list ->
  unitSource
val field_lookup : 
  Geninterp.Val.t ->
  EConstr.constr list ->
  EConstr.constr list ->
  EConstr.constr ->
  unit Proofview.tactic sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >