diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 20:38:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | 873281c256fc33941d93044acc3db8eda0a148ee (patch) | |
| tree | 2104c16c197b2cc9a8c9cc903818691b6eb1a3a7 /plugins/funind | |
| parent | 7dc04f0244aeb277b62070f87590cbc2cafd8396 (diff) | |
[proof] Move declaration hooks to DeclareDef.
This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
4 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8af5dc818b..08acb754f7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin in let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in evd := sigma; - let hook = Lemmas.mk_hook (hook new_principle_type) in + let hook = DeclareDef.Hook.make (hook new_principle_type) in let lemma = Lemmas.start_lemma new_princ_name diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7683ce1757..732a0d818f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -137,7 +137,7 @@ let save id const ?hook uctx (locality,_,kind) = let kn = declare_constant id ~local (DefinitionEntry const, k) in ConstRef kn in - Lemmas.call_hook ?hook ~fix_exn uctx [] locality r; + DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 4078c34331..8dd990775b 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -45,7 +45,7 @@ val jmeq_refl : unit -> EConstr.constr val save : Id.t -> Evd.side_effects Entries.definition_entry - -> ?hook:Lemmas.declaration_hook + -> ?hook:DeclareDef.Hook.t -> UState.t -> Decl_kinds.goal_kind -> unit diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2b5c0a01db..8169ff459f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1371,7 +1371,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let lemma = Lemmas.start_lemma na Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) - sigma gls_type ~hook:(Lemmas.mk_hook hook) in + sigma gls_type ~hook:(DeclareDef.Hook.make hook) in let lemma = if Indfun_common.is_strict_tcc () then fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma @@ -1592,5 +1592,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type term_id using_lemmas (List.length res_vars) - evd (Lemmas.mk_hook hook)) + evd (DeclareDef.Hook.make hook)) () |