diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 732a0d818f..17c79e0e6c 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -118,14 +118,13 @@ let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (* Copy of the standard save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) -open Entries open Decl_kinds open Declare let definition_message = Declare.definition_message let save id const ?hook uctx (locality,_,kind) = - let fix_exn = Future.fix_exn_of const.const_entry_body in + let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in let r = match locality with | Discharge -> let k = Kindops.logical_kind_of_goal_kind kind in @@ -134,7 +133,7 @@ let save id const ?hook uctx (locality,_,kind) = VarRef id | Global local -> let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id ~local (DefinitionEntry const, k) in + let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in ConstRef kn in DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r; |