Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

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))