package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20
doc/rocq-runtime.proofs/Subproof/index.html
Module SubproofSource
Source
val refine_by_tactic :
name:Names.Id.t ->
poly:PolyFlags.t ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
unit Proofview.tactic ->
EConstr.constr * Evd.evar_mapA variant of Proof.solve that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may occur. Ideally all code using this function should be rewritten in the monad.
Source
val build_by_tactic :
Environ.env ->
uctx:UState.t ->
poly:PolyFlags.t ->
typ:EConstr.types ->
unit Proofview.tactic ->
Constr.constr * Constr.types * UState.named_universes_entry * bool * UState.tSemantics of this function is a bit dubious, use with care
Source
val build_by_tactic_opt :
Environ.env ->
uctx:UState.t ->
poly:PolyFlags.t ->
typ:EConstr.types ->
unit Proofview.tactic ->
(Constr.constr
* Constr.types
* UState.named_universes_entry
* bool
* UState.t)
optionSame as above but returns None rather than an exception if the proof is not finished
Source
val declare_abstract :
name:Names.Id.t ->
poly:PolyFlags.t ->
sign:EConstr.named_context ->
secsign:Environ.named_context_val ->
opaque:bool ->
solve_tac:unit Proofview.tactic ->
Environ.env ->
Evd.evar_map ->
EConstr.t ->
Evd.evar_map * EConstr.t * EConstr.t list * boolSource
val shrink_entry :
('a, 'b, 'c) Context.Named.Declaration.pt list ->
Constr.constr ->
Constr.types ->
Constr.constr * Constr.constr * EConstr.t list