diff options
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 90327da6c..3c1f6a415 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -18,8 +18,8 @@ open Util let body_of_constant cb = match cb.const_body with | Undef _ -> None - | Def c -> Some c - | OpaqueDef lc -> Some (force_lazy_constr lc) + | Def c -> Some (Lazyconstr.force c) + | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc) let constant_has_body cb = match cb.const_body with | Undef _ -> false @@ -84,14 +84,8 @@ let hcons_const_type = function let hcons_const_def = function | Undef inl -> Undef inl - | Def l_constr -> - let constr = force l_constr in - Def (from_val (Term.hcons_constr constr)) - | OpaqueDef lc -> - if lazy_constr_is_val lc then - let constr = force_opaque lc in - OpaqueDef (opaque_from_val (Term.hcons_constr constr)) - else OpaqueDef lc + | Def cs -> Def (from_val (Term.hcons_constr (Lazyconstr.force cs))) + | OpaqueDef lc -> OpaqueDef (Lazyconstr.hcons_lazy_constr lc) let hcons_const_body cb = { cb with |