diff options
Diffstat (limited to 'vernac/lemmas.mli')
-rw-r--r-- | vernac/lemmas.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 398f7d6d0..c9e4876ee 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -21,13 +21,13 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (EConstr.types -> unit) -> unit -val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> +val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> +val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> @@ -39,7 +39,7 @@ val start_proof_com : unit declaration_hook -> unit val start_proof_with_initialization : - goal_kind -> Evd.evar_map -> Univdecls.universe_decl -> + goal_kind -> Evd.evar_map -> UState.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list |