diff options
Diffstat (limited to 'stm/lemmas.mli')
| -rw-r--r-- | stm/lemmas.mli | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 6556aa229..dca6afe19 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -24,11 +24,15 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (types -> unit) -> unit -val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof : Id.t -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> unit @@ -40,6 +44,11 @@ val start_proof_with_initialization : (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit +val universe_proof_terminator : + Proof_global.lemma_possible_guards -> + (Proof_global.proof_universes option -> unit declaration_hook) -> + Proof_global.proof_terminator + val standard_proof_terminator : Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator |