aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/tacexpr.mli2
-rw-r--r--lib/future.ml7
-rw-r--r--lib/future.mli5
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--stm/lemmas.ml16
-rw-r--r--stm/lemmas.mli8
-rw-r--r--stm/stm.ml2
-rw-r--r--tactics/rewrite.ml2
-rw-r--r--toplevel/class.ml4
-rw-r--r--toplevel/class.mli4
-rw-r--r--toplevel/classes.ml4
-rw-r--r--toplevel/command.ml14
-rw-r--r--toplevel/command.mli4
-rw-r--r--toplevel/obligations.ml14
-rw-r--r--toplevel/obligations.mli6
-rw-r--r--toplevel/vernacentries.ml4
22 files changed, 59 insertions, 57 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7895ddbf4..530213b7c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -272,5 +272,3 @@ type raw_tactic_arg =
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
-
-type 'a declaration_hook = 'a Future.hook
diff --git a/lib/future.ml b/lib/future.ml
index 960363e25..77386a1a9 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -91,13 +91,6 @@ let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn
-type 'a hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
-let mk_hook hook = hook
-let call_hook fix_exn hook l c =
- try hook l c
- with e when Errors.noncritical e ->
- let e = Errors.push e in
- raise (fix_exn e)
let default_force () = raise NotReady
let assignement ck = fun v ->
diff --git a/lib/future.mli b/lib/future.mli
index 41f5e185c..c4b55db25 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -91,11 +91,6 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
* is split into two parts, the lazy one (the future) and the eagher one
* (the hook), both performing some computations for the same state id. *)
val fix_exn_of : 'a computation -> fix_exn
-type 'a hook
-val mk_hook :
- (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a hook
-val call_hook :
- fix_exn -> 'a hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
(* Run remotely, returns the function to assign. Optionally tekes a function
that is called when forced. The default one is to raise NotReady.
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 714192f53..9589e51f4 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -988,7 +988,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
(mk_equation_id f_id)
(Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
(lemma_type, (*FIXME*) Univ.ContextSet.empty)
- (Future.mk_hook (fun _ _ -> ()));
+ (Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
Lemmas.save_proof (Vernacexpr.Proved(false,None))
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 65a262707..f4a062732 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -290,7 +290,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
let new_princ_name =
next_ident_away_in_goal (Id.of_string "___________princ_________") []
in
- let hook = Future.mk_hook (hook new_principle_type) in
+ let hook = Lemmas.mk_hook (hook new_principle_type) in
begin
Lemmas.start_proof
new_princ_name
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 8c8d7a667..e10ed49ed 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -352,7 +352,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
| [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition)
- bl None body (Some ret_type) (Future.mk_hook (fun _ _ -> ()))
+ bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()))
| _ ->
Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b923260c2..76f8c6d21 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -161,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook =
(locality, ConstRef kn)
in
if with_clean then Pfedit.delete_current_proof ();
- Ephemeron.iter_opt hook (fun f -> Future.call_hook fix_exn f l r);
+ Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
definition_message id
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 3fafeadc1..67ddf3741 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,7 @@ val jmeq : unit -> Term.constr
val jmeq_refl : unit -> Term.constr
val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind ->
- unit Tacexpr.declaration_hook Ephemeron.key -> unit
+ unit Lemmas.declaration_hook Ephemeron.key -> unit
(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
abort the proof
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9558923f6..2c153becf 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1080,7 +1080,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Lemmas.start_proof lem_id
(Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
- (Future.mk_hook (fun _ _ -> ()));
+ (Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))));
@@ -1133,7 +1133,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Lemmas.start_proof lem_id
(Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
- (Future.mk_hook (fun _ _ -> ()));
+ (Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i))));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 08d8ca391..d8f006f51 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1320,7 +1320,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
na
(Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
(gls_type, ctx)
- (Future.mk_hook hook);
+ (Lemmas.mk_hook hook);
if Indfun_common.is_strict_tcc ()
then
ignore (by (Proofview.V82.tactic (tclIDTAC)))
@@ -1417,7 +1417,7 @@ let (com_eqn : int -> Id.t ->
(Lemmas.start_proof eq_name (Global, false, Proof Lemma)
~sign:(Environ.named_context_val env)
(equation_lemma_type, (*FIXME*)Univ.ContextSet.empty)
- (Future.mk_hook (fun _ _ -> ()));
+ (Lemmas.mk_hook (fun _ _ -> ()));
ignore (by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
(fun x ->
@@ -1537,5 +1537,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- ctx (Future.mk_hook hook))
+ ctx (Lemmas.mk_hook hook))
()
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 493b874ae..5f580bca5 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -32,6 +32,14 @@ open Constrexpr
open Constrintern
open Impargs
+type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
+let mk_hook hook = hook
+let call_hook fix_exn hook l c =
+ try hook l c
+ with e when Errors.noncritical e ->
+ let e = Errors.push e in
+ raise (fix_exn e)
+
(* Support for mutually proved theorems *)
let retrieve_first_recthm = function
@@ -184,7 +192,7 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
let kn = declare_constant id ~local (DefinitionEntry const, k) in
(locality, ConstRef kn) in
definition_message id;
- Future.call_hook fix_exn hook l r
+ call_hook fix_exn hook l r
let default_thm_id = Id.of_string "Unnamed_thm"
@@ -286,7 +294,7 @@ let admit hook () =
str "declared as an axiom.")
in
let () = assumption_message id in
- Future.call_hook (fun exn -> exn) hook Global (ConstRef kn)
+ call_hook (fun exn -> exn) hook Global (ConstRef kn)
(* Starting a goal *)
@@ -401,8 +409,8 @@ let start_proof_with_initialization kind recguard thms snl hook =
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
- Future.call_hook (fun exn -> exn) hook strength ref) thms_data in
- start_proof id kind t ?init_tac (Future.mk_hook hook) ~compute_guard:guard
+ call_hook (fun exn -> exn) hook strength ref) thms_data in
+ start_proof id kind t ?init_tac (mk_hook hook) ~compute_guard:guard
let start_proof_com kind thms hook =
let env0 = Global.env () in
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 8f5c75976..d0dd2d333 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -14,6 +14,14 @@ open Tacexpr
open Vernacexpr
open Pfedit
+type 'a declaration_hook
+
+val mk_hook :
+ (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
+
+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
diff --git a/stm/stm.ml b/stm/stm.ml
index c70838990..5733b0c32 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -764,7 +764,7 @@ end = struct
(* The original terminator, a hook, has not been saved in the .vi*)
Proof_global.set_terminator
(Lemmas.standard_proof_terminator []
- (Future.mk_hook (fun _ _ -> ())));
+ (Lemmas.mk_hook (fun _ _ -> ())));
let proof = Proof_global.close_proof (fun x -> x) in
vernac_interp eop ~proof
{ verbose = false; loc;
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1c98ec21d..2970eece8 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1878,7 +1878,7 @@ let add_morphism_infer glob m n =
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
in
- let hook = Future.mk_hook hook in
+ let hook = Lemmas.mk_hook hook in
Flags.silently
(fun () ->
Lemmas.start_proof instance_id kind (instance, ctx) hook;
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 1d8529051..635b1c52c 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -304,7 +304,7 @@ let add_coercion_hook poly local ref =
let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
Flags.if_verbose msg_info msg
-let add_coercion_hook poly = Future.mk_hook (add_coercion_hook poly)
+let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
let add_subclass_hook poly local ref =
let stre = match local with
@@ -315,4 +315,4 @@ let add_subclass_hook poly local ref =
let cl = class_of_global ref in
try_add_new_coercion_subclass cl stre poly
-let add_subclass_hook poly = Future.mk_hook (add_subclass_hook poly)
+let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly)
diff --git a/toplevel/class.mli b/toplevel/class.mli
index d472bd984..d374610c3 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -41,8 +41,8 @@ val try_add_new_coercion_with_source : global_reference -> local:bool ->
val try_add_new_identity_coercion : Id.t -> local:bool ->
Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
-val add_coercion_hook : Decl_kinds.polymorphic -> unit Tacexpr.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
-val add_subclass_hook : Decl_kinds.polymorphic -> unit Tacexpr.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
val class_of_global : global_reference -> cl_typ
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5d1a0a43b..99c3e977c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -294,7 +294,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
in obls, Some constr, typ
| None -> [||], None, termtype
in
- let hook = Future.mk_hook hook in
+ let hook = Lemmas.mk_hook hook in
let ctx = Evd.universe_context_set evm in
ignore (Obligations.add_definition id ?term:constr
typ ctx ~kind:(Global,poly,Instance) ~hook obls);
@@ -303,7 +303,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
(Flags.silently
(fun () ->
Lemmas.start_proof id kind (termtype, Evd.universe_context_set evm)
- (Future.mk_hook
+ (Lemmas.mk_hook
(fun _ -> instance_hook k pri global imps ?hook));
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b49fe40a0..39fe8f4ab 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -163,7 +163,7 @@ let declare_definition ident (local, p, k) ce imps hook =
VarRef ident
| Discharge | Local | Global ->
declare_global_definition ident ce local k imps in
- Future.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
+ Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
let _ = Obligations.declare_definition_ref := declare_definition
@@ -187,8 +187,8 @@ let do_definition ident k bl red_option c ctypopt hook =
ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
ignore(declare_definition ident k ce imps
- (Future.mk_hook
- (fun l r -> Future.call_hook (fun exn -> exn) hook l r;r)))
+ (Lemmas.mk_hook
+ (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -692,7 +692,7 @@ let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
- declare_definition f kind ce imps (Future.mk_hook (fun _ r -> r))
+ declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
let _ = Obligations.declare_fix_ref := declare_fix
@@ -900,7 +900,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
Impargs.declare_manual_implicits false gr [impls]
in hook, recname, typ
in
- let hook = Future.mk_hook hook in
+ let hook = Lemmas.mk_hook hook in
let fullcoqc = Evarutil.nf_evar !evdref def in
let fullctyp = Evarutil.nf_evar !evdref typ in
Obligations.check_evars env !evdref;
@@ -994,7 +994,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
Option.map (List.map Proofview.V82.tactic) init_tac
in
Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
- (Some(false,indexes,init_tac)) thms None (Future.mk_hook (fun _ _ -> ()))
+ (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -1028,7 +1028,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
Option.map (List.map Proofview.V82.tactic) init_tac
in
Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
- (Some(true,[],init_tac)) thms None (Future.mk_hook (fun _ _ -> ()))
+ (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 41cb5baa3..e48a77000 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -34,11 +34,11 @@ val interp_definition :
val declare_definition : Id.t -> definition_kind ->
definition_entry -> Impargs.manual_implicits ->
- Globnames.global_reference declaration_hook -> Globnames.global_reference
+ Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
val do_definition : Id.t -> definition_kind ->
local_binder list -> red_expr option -> constr_expr ->
- constr_expr option -> unit declaration_hook -> unit
+ constr_expr option -> unit Lemmas.declaration_hook -> unit
(** {6 Parameters/Assumptions} *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 00fc3e0ce..1543c5e87 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -333,7 +333,7 @@ type program_info = {
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
- prg_hook : unit Tacexpr.declaration_hook;
+ prg_hook : unit Lemmas.declaration_hook;
}
let assumption_message = Declare.assumption_message
@@ -535,8 +535,8 @@ let declare_definition prg =
progmap_remove prg;
!declare_definition_ref prg.prg_name
prg.prg_kind ce prg.prg_implicits
- (Future.mk_hook (fun l r ->
- Future.call_hook (fun exn -> exn) prg.prg_hook l r; r))
+ (Lemmas.mk_hook (fun l r ->
+ Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r))
open Pp
@@ -607,7 +607,7 @@ let declare_mutual_definition l =
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
- Future.call_hook (fun exn -> exn) first.prg_hook local gr;
+ Lemmas.call_hook (fun exn -> exn) first.prg_hook local gr;
List.iter progmap_remove l; kn
let shrink_body c =
@@ -816,7 +816,7 @@ let rec solve_obligation prg num tac =
let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
Lemmas.start_proof_univs obl.obl_name kind
(Universes.subst_opt_univs_constr prg.prg_subst obl.obl_type, ctx)
- (fun (subst, ctx) -> Future.mk_hook (fun strength gr ->
+ (fun (subst, ctx) -> Lemmas.mk_hook (fun strength gr ->
let cst = match gr with ConstRef cst -> cst | _ -> assert false in
let obl =
let transparent = evaluable_constant cst (Global.env ()) in
@@ -977,7 +977,7 @@ let show_term n =
++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?(hook=Future.mk_hook (fun _ _ -> ())) obls =
+ ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) obls =
let info = str (Id.to_string n) ++ str " has type-checked" in
let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
@@ -995,7 +995,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
| _ -> res)
let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
- ?(hook=Future.mk_hook (fun _ _ -> ())) notations fixkind =
+ ?(hook=Lemmas.mk_hook (fun _ _ -> ())) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index f03e6c446..bf186193a 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -23,7 +23,7 @@ val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t ->
val declare_definition_ref :
(Id.t -> definition_kind ->
Entries.definition_entry -> Impargs.manual_implicits
- -> global_reference declaration_hook -> global_reference) ref
+ -> global_reference Lemmas.declaration_hook -> global_reference) ref
val check_evars : env -> evar_map -> unit
@@ -69,7 +69,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
?reduce:(Term.constr -> Term.constr) ->
- ?hook:unit Tacexpr.declaration_hook -> obligation_info -> progress
+ ?hook:unit Lemmas.declaration_hook -> obligation_info -> progress
type notations =
(Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -85,7 +85,7 @@ val add_mutual_definitions :
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(Term.constr -> Term.constr) ->
- ?hook:unit Tacexpr.declaration_hook ->
+ ?hook:unit Lemmas.declaration_hook ->
notations ->
fixpoint_kind -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1fdf95c0f..8e424a96f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -452,12 +452,12 @@ let start_proof_and_print k l hook =
start_proof_com k l hook;
print_subgoals ()
-let no_hook = Future.mk_hook (fun _ _ -> ())
+let no_hook = Lemmas.mk_hook (fun _ _ -> ())
let vernac_definition_hook p = function
| Coercion -> Class.add_coercion_hook p
| CanonicalStructure ->
- Future.mk_hook (fun _ -> Recordops.declare_canonical_structure)
+ Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
| SubClass -> Class.add_subclass_hook p
| _ -> no_hook
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 00:39:30 +0000