diff options
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 707c46048b..5686c4071d 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -56,8 +56,9 @@ let constant_is_polymorphic cb = | Monomorphic_const _ -> false | Polymorphic_const _ -> true + let constant_has_body cb = match cb.const_body with - | Undef _ -> false + | Undef _ | Primitive _ -> false | Def _ | OpaqueDef _ -> true let constant_polymorphic_context cb = @@ -67,7 +68,7 @@ let constant_polymorphic_context cb = let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true - | Undef _ | Def _ -> false + | Undef _ | Def _ | Primitive _ -> false (** {7 Constant substitutions } *) @@ -83,7 +84,7 @@ let subst_const_type sub arity = (** No need here to check for physical equality after substitution, at least for Def due to the delayed substitution [subst_constr_subst]. *) let subst_const_def sub def = match def with - | Undef _ -> def + | Undef _ | Primitive _ -> def | Def c -> Def (subst_constr sub c) | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) @@ -119,6 +120,7 @@ let hcons_rel_context l = List.Smart.map hcons_rel_decl l let hcons_const_def = function | Undef inl -> Undef inl + | Primitive p -> Primitive p | Def l_constr -> let constr = force_constr l_constr in Def (from_val (Constr.hcons constr)) |