diff options
Diffstat (limited to 'vernac/lemmas.mli')
| -rw-r--r-- | vernac/lemmas.mli | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index d06b8fd14..a9c0d99f3 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -9,7 +9,6 @@ open Names open Term open Decl_kinds -open Pfedit type 'a declaration_hook val mk_hook : @@ -21,16 +20,16 @@ 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:universe_binders -> goal_kind -> Evd.evar_map -> - ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> +val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> 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:lemma_possible_guards -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.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) -> +val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit val start_proof_com : @@ -40,8 +39,8 @@ val start_proof_com : val start_proof_with_initialization : goal_kind -> Evd.evar_map -> - (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - ((Id.t (* name of thm *) * universe_binders option) * + (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> + ((Id.t (* name of thm *) * Proof_global.universe_binders option) * (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit |