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 6b45ed933..d06b8fd14 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -19,17 +19,17 @@ val call_hook : Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a (** A hook start_proof calls on the type of the definition being started *) -val set_start_hook : (types -> unit) -> unit +val set_start_hook : (EConstr.types -> unit) -> unit val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> + ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> + ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit |