Merge PR #6914: Primitive integers

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

4 files changed, 9 insertions, 4 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 24d161d00a..8493119ee5 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -73,6 +73,7 @@ let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
 let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
+let mkInt i = of_kind (Int i)
 
 let mkRef (gr,u) = let open GlobRef in match gr with
   | ConstRef c -> mkConstU (c,u)
@@ -81,6 +82,7 @@ let mkRef (gr,u) = let open GlobRef in match gr with
   | VarRef x -> mkVar x
 
 let applist (f, arg) = mkApp (f, Array.of_list arg)
+let applistc f arg = mkApp (f, Array.of_list arg)
 
 let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
 let isVar sigma c = match kind sigma c with Var _ -> true | _ -> false
@@ -328,7 +330,7 @@ let iter_with_full_binders sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> ()
+    | Construct _ | Int _) -> ()
   | Cast (c,_,t) -> f n c; f n t
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 49cbc4d7e5..2f4cf7d5d0 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -124,10 +124,12 @@ val mkCase : case_info * t * t * t array -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> t -> t
+val mkInt : Uint63.t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
 
 val applist : t * t list -> t
+val applistc : t -> t list -> t
 
 val mkProd_or_LetIn : rel_declaration -> t -> t
 val mkLambda_or_LetIn : rel_declaration -> t -> t
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 018eca1ba2..294b61fd3d 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
 	Some (match lna.(i) with Name id -> id | _ -> assert false)
-    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
+    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None
   in
   hdrec c
 
@@ -163,6 +163,7 @@ let hdchar env sigma c =
 	lowercase_first_char id
     | Evar _ (* We could do better... *)
     | Meta _ | Case (_, _, _, _) -> "y"
+    | Int _ -> "i"
   in
   hdrec 0 c
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 3e902129f3..579100ad4c 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -600,7 +600,7 @@ let map_constr_with_binders_left_to_right sigma g f l c =
   let open EConstr in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
+    | Construct _ | Int _) -> c
   | Cast (b,k,t) -> 
     let b' = f l b in 
     let t' = f l t in
@@ -681,7 +681,7 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
   let open EConstr in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> cstr
+    | Construct _ | Int _) -> cstr
   | Cast (c,k, t) ->
       let c' = f l c in
       let t' = f l t in