aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/lemmas.mli')
-rw-r--r--vernac/lemmas.mli17
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