Merge PR #6914: Primitive integers

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

21 files changed, 373 insertions, 138 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index f8289f558c..e27fc536eb 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -38,6 +38,10 @@ open Esubst
  *          the bindings S, and then applied to args. Here again,
  *          weak reduction.
  *  CONSTR(c,args) is the constructor [c] applied to [args].
+ *  PRIMITIVE(cop,args) represent a particial application of
+ *          a primitive, or a fully applied primitive
+ *          which does not reduce.
+ *          cop is the constr representing op.
  *
  *)
 type cbv_value =
@@ -48,6 +52,7 @@ type cbv_value =
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
   | CONSTR of constructor Univ.puniverses * cbv_value array
+  | PRIMITIVE of CPrimitives.t * constr * cbv_value array
 
 (* type of terms with a hole. This hole can appear only under App or Case.
  *   TOP means the term is considered without context
@@ -90,6 +95,9 @@ let rec shift_value n = function
       COFIXP (cofix,subs_shft (n,s), Array.map (shift_value n) args)
   | CONSTR (c,args) ->
       CONSTR (c, Array.map (shift_value n) args)
+  | PRIMITIVE(op,c,args) ->
+      PRIMITIVE(op,c,Array.map (shift_value n) args)
+
 let shift_value n v =
   if Int.equal n 0 then v else shift_value n v
 
@@ -109,10 +117,11 @@ let contract_cofixp env (i,(_,_,bds as bodies)) =
   let n = Array.length bds in
   subs_cons(Array.init n make_body, env), bds.(i)
 
-let make_constr_ref n = function
+let make_constr_ref n k t =
+  match k with
   | RelKey p -> mkRel (n+p)
-  | VarKey id -> mkVar id
-  | ConstKey cst -> mkConstU cst
+  | VarKey id -> t
+  | ConstKey cst -> t
 
 (* Adds an application list. Collapse APPs! *)
 let stack_app appl stack =
@@ -136,7 +145,7 @@ let mkSTACK = function
 
 type cbv_infos = {
   env : Environ.env;
-  tab : cbv_value KeyTable.t;
+  tab : cbv_value Declarations.constant_def KeyTable.t;
   reds : RedFlags.reds;
   sigma : Evd.evar_map
 }
@@ -159,7 +168,8 @@ let strip_appl head stack =
     | FIXP (fix,env,app) -> (FIXP(fix,env,[||]), stack_app app stack)
     | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[||]), stack_app app stack)
     | CONSTR (c,app) -> (CONSTR(c,[||]), stack_app app stack)
-    | _ -> (head, stack)
+    | PRIMITIVE(op,c,app) -> (PRIMITIVE(op,c,[||]), stack_app app stack)
+    | VAL _ | STACK _ | CBN _ | LAM _ -> (head, stack)
 
 
 (* Tests if fixpoint reduction is possible. *)
@@ -189,6 +199,60 @@ let get_debug_cbv = Goptions.declare_bool_option_and_ref
     ~name:"cbv visited constants display"
     ~key:["Debug";"Cbv"]
 
+(* Reduction of primitives *)
+
+open Primred
+
+module VNativeEntries =
+  struct
+
+    type elem = cbv_value
+    type args = cbv_value array
+    type evd = unit
+
+    let get = Array.get
+
+    let get_int () e =
+      match e with
+      | VAL(_, ci) ->
+          (match kind ci with
+          | Int i -> i
+          | _ -> raise Primred.NativeDestKO)
+      | _ -> raise Primred.NativeDestKO
+
+    let mkInt env i = VAL(0, mkInt i)
+
+    let mkBool env b =
+      let (ct,cf) = get_bool_constructors env in
+      CONSTR(Univ.in_punivs (if b then ct else cf), [||])
+
+    let int_ty env = VAL(0, mkConst @@ get_int_type env)
+
+    let mkCarry env b e =
+      let (c0,c1) = get_carry_constructors env in
+      CONSTR(Univ.in_punivs (if b then c1 else c0), [|int_ty env;e|])
+
+    let mkIntPair env e1 e2 =
+      let int_ty = int_ty env in
+      let c = get_pair_constructor env in
+      CONSTR(Univ.in_punivs c, [|int_ty;int_ty;e1;e2|])
+
+    let mkLt env =
+      let (_eq,lt,_gt) = get_cmp_constructors env in
+      CONSTR(Univ.in_punivs lt, [||])
+
+    let mkEq env =
+      let (eq,_lt,_gt) = get_cmp_constructors env in
+      CONSTR(Univ.in_punivs eq, [||])
+
+    let mkGt env =
+      let (_eq,_lt,gt) = get_cmp_constructors env in
+      CONSTR(Univ.in_punivs gt, [||])
+
+  end
+
+module VredNative = RedNative(VNativeEntries)
+
 let debug_pr_key = function
   | ConstKey (sp,_) -> Names.Constant.print sp
   | VarKey id -> Names.Id.print id
@@ -225,6 +289,8 @@ and reify_value = function (* reduction under binders *)
     mkApp (apply_env env cofix, Array.map reify_value args)
   | CONSTR (c,args) ->
       mkApp(mkConstructU c, Array.map reify_value args)
+  | PRIMITIVE(op,c,args) ->
+      mkApp(c, Array.map reify_value args)
 
 and apply_env env t =
   match kind t with
@@ -277,14 +343,14 @@ let rec norm_head info env t stack =
         | Inl (0,v)      -> strip_appl v stack
         | Inl (n,v)      -> strip_appl (shift_value n v) stack
         | Inr (n,None)   -> (VAL(0, mkRel n), stack)
-        | Inr (n,Some p) -> norm_head_ref (n-p) info env stack (RelKey p))
+        | Inr (n,Some p) -> norm_head_ref (n-p) info env stack (RelKey p) t)
 
-  | Var id -> norm_head_ref 0 info env stack (VarKey id)
+  | Var id -> norm_head_ref 0 info env stack (VarKey id) t
 
   | Const sp ->
     Reductionops.reduction_effect_hook info.env info.sigma
       (fst sp) (lazy (reify_stack t stack));
-    norm_head_ref 0 info env stack (ConstKey sp)
+    norm_head_ref 0 info env stack (ConstKey sp) t
 
   | LetIn (_, b, _, c) ->
       (* zeta means letin are contracted; delta without zeta means we *)
@@ -315,22 +381,23 @@ let rec norm_head info env t stack =
   | Construct c -> (CONSTR(c, [||]), stack)
 
   (* neutral cases *)
-  | (Sort _ | Meta _ | Ind _) -> (VAL(0, t), stack)
+  | (Sort _ | Meta _ | Ind _ | Int _) -> (VAL(0, t), stack)
   | Prod _ -> (CBN(t,env), stack)
 
-and norm_head_ref k info env stack normt =
+and norm_head_ref k info env stack normt t =
   if red_set_ref info.reds normt then
     match cbv_value_cache info normt with
-      | Some body ->
+      | Declarations.Def body ->
          if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
          strip_appl (shift_value k body) stack
-      | None ->
+      | Declarations.Primitive op -> (PRIMITIVE(op,t,[||]),stack)
+      | Declarations.OpaqueDef _ | Declarations.Undef _ ->
          if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
-         (VAL(0,make_constr_ref k normt),stack)
+         (VAL(0,make_constr_ref k normt t),stack)
   else
     begin
       if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
-      (VAL(0,make_constr_ref k normt),stack)
+      (VAL(0,make_constr_ref k normt t),stack)
     end
 
 (* cbv_stack_term performs weak reduction on constr t under the subs
@@ -392,32 +459,58 @@ and cbv_stack_value info env = function
     | (COFIXP(cofix,env,[||]), APP(appl,TOP)) -> COFIXP(cofix,env,appl)
     | (CONSTR(c,[||]), APP(appl,TOP)) -> CONSTR(c,appl)
 
+    (* primitive apply to arguments *)
+    | (PRIMITIVE(op,c,[||]), APP(appl,stk)) ->
+      let nargs = CPrimitives.arity op in
+      let len = Array.length appl in
+      if nargs <= len then
+        let args =
+          if len = nargs then appl
+          else Array.sub appl 0 nargs in
+        let stk =
+          if nargs < len then
+            stack_app (Array.sub appl nargs (len - nargs)) stk
+          else stk in
+        match VredNative.red_prim info.env () op args with
+        | Some (CONSTR (c, args)) ->
+          (* args must be moved to the stack to allow future reductions *)
+          cbv_stack_value info env (CONSTR(c, [||]), stack_app args stk)
+        | Some v ->  cbv_stack_value info env (v,stk)
+        | None -> mkSTACK(PRIMITIVE(op,c,args), stk)
+      else (* partical application *)
+              (assert (stk = TOP);
+               PRIMITIVE(op,c,appl))
+
     (* definitely a value *)
     | (head,stk) -> mkSTACK(head, stk)
 
-and cbv_value_cache info ref = match KeyTable.find info.tab ref with
-| v -> Some v
-| exception Not_found ->
-  try
-    let body = match ref with
-    | RelKey n ->
-      let open Context.Rel.Declaration in
-      begin match Environ.lookup_rel n info.env with
-      | LocalDef (_, c, _) -> lift n c
-      | LocalAssum _ -> raise Not_found
-      end
-    | VarKey id ->
-      let open Context.Named.Declaration in
-      begin match Environ.lookup_named id info.env with
-      | LocalDef (_, c, _) -> c
-      | LocalAssum _ -> raise Not_found
-      end
-    | ConstKey cst -> Environ.constant_value_in info.env cst
+and cbv_value_cache info ref =
+  try KeyTable.find info.tab ref with
+    Not_found ->
+    let v =
+      try
+        let body = match ref with
+          | RelKey n ->
+            let open Context.Rel.Declaration in
+            begin match Environ.lookup_rel n info.env with
+              | LocalDef (_, c, _) -> lift n c
+              | LocalAssum _ -> raise Not_found
+            end
+          | VarKey id ->
+            let open Context.Named.Declaration in
+            begin match Environ.lookup_named id info.env with
+              | LocalDef (_, c, _) -> c
+              | LocalAssum _ -> raise Not_found
+            end
+          | ConstKey cst -> Environ.constant_value_in info.env cst
+        in
+        let v = cbv_stack_term info TOP (subs_id 0) body in
+        Declarations.Def v
+      with
+      | Environ.NotEvaluableConst (Environ.IsPrimitive op) -> Declarations.Primitive op
+      | Not_found | Environ.NotEvaluableConst _ -> Declarations.Undef None
     in
-    let v = cbv_stack_term info TOP (subs_id 0) body in
-    let () = KeyTable.add info.tab ref v in
-    Some v
-  with Not_found | Environ.NotEvaluableConst _ -> None
+    KeyTable.add info.tab ref v; v
 
 (* When we are sure t will never produce a redex with its stack, we
  * normalize (even under binders) the applied terms and we build the
@@ -471,6 +564,8 @@ and cbv_norm_value info = function (* reduction under binders *)
          Array.map (cbv_norm_value info) args)
   | CONSTR (c,args) ->
       mkApp(mkConstructU c, Array.map (cbv_norm_value info) args)
+  | PRIMITIVE(op,c,args) ->
+      mkApp(c,Array.map (cbv_norm_value info) args)
 
 (* with profiling *)
 let cbv_norm infos constr =
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 83844c95a7..0a1e771921 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -36,6 +36,7 @@ type cbv_value =
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
   | CONSTR of constructor Univ.puniverses * cbv_value array
+  | PRIMITIVE of CPrimitives.t * Constr.t * cbv_value array
 
 and cbv_stack =
   | TOP
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 032e4bbf85..94257fedd7 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -410,9 +410,10 @@ let matches_core env sigma allow_bound_rels
 
       | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
          Array.fold_left2 (sorec ctx env) subst args1 args2
+      | PInt i1, Int i2 when Uint63.equal i1 i2 -> subst
       | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
          | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
-         | PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure
+         | PFix _ | PCoFix _| PEvar _ | PInt _), _ -> raise PatternMatchingFailure
 
   in
   sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c
@@ -530,7 +531,7 @@ let sub_match ?(closed=true) env sigma pat c =
       aux env term mk_ctx next
     with Retyping.RetypeError _ -> next ()
     end
-  | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
+  | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ | Int _ ->
     next ()
   in
   here next
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c7cc2dbc8a..6746e4b902 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -766,6 +766,7 @@ and detype_r d flags avoid env sigma t =
           p c bl
     | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef
     | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef
+    | Int i -> GInt i
 
 and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
@@ -959,6 +960,7 @@ let rec subst_glob_constr subst = DAst.map (function
   | GSort _
   | GVar _
   | GEvar _
+  | GInt _
   | GPatVar _ as raw -> raw
 
   | GApp (r,rl) as raw ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ed28cc7725..aa30ed8d2e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -107,7 +107,7 @@ let flex_kind_of_term ts env evd c sk =
       Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c)
     | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c
     | Evar ev -> Flexible ev
-    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid
+    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ -> Rigid
     | Meta _ -> Rigid
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
     | Cast _ | App _ | Case _ -> assert false
@@ -127,7 +127,7 @@ let occur_rigidly (evk,_ as ev) evd t =
   let rec aux t =
     match EConstr.kind evd t with
     | App (f, c) -> if aux f then Array.exists aux c else false
-    | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
+    | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ | Int _ -> true
     | Proj (p, c) -> not (aux c)
     | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false
     | Cast (p, _, _) -> aux p
@@ -769,7 +769,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
              only if necessary) or the second argument is potentially
              usable as a canonical projection or canonical value *)
           let rec is_unnamed (hd, args) = match EConstr.kind i hd with
-            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) ->
+            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _) ->
 	      Stack.not_purely_applicative args
             | (CoFix _|Meta _|Rel _)-> true
             | Evar _ -> Stack.not_purely_applicative args
@@ -887,8 +887,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
 	| Const _, Const _
 	| Ind _, Ind _ 
-	| Construct _, Construct _ ->
-	  rigids env evd sk1 term1 sk2 term2
+        | Construct _, Construct _
+        | Int _, Int _ ->
+          rigids env evd sk1 term1 sk2 term2
 
 	| Construct u, _ ->
 	  eta_constructor ts env evd sk1 u sk2 term2
@@ -923,9 +924,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2'))
 	  end
 
-	| (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ ->
-	  UnifFailure (evd,NotSameHead)
-	| _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _) ->
+        | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _), _ ->
 	  UnifFailure (evd,NotSameHead)
 
 	| (App _ | Cast _ | Case _ | Proj _), _ -> assert false
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e14766f370..6b61b1452e 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -152,8 +152,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     Namegen.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
+  | GInt i1, GInt i2 -> Uint63.equal i1 i2
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
-     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ ), _ -> false
+     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ |
+     GInt _), _ -> false
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
@@ -214,7 +216,7 @@ let map_glob_constr_left_to_right f = DAst.map (function
       let comp1 = f c in
       let comp2 = map_cast_type f k in
       GCast (comp1,comp2)
-  | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
+  | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) as x -> x
   )
 
 let map_glob_constr = map_glob_constr_left_to_right
@@ -246,9 +248,8 @@ let fold_glob_constr f acc = DAst.with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
     f acc c
-  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) -> acc
   )
-
 let fold_return_type_with_binders f g v acc (na,tyopt) =
   Option.fold_left (f (Name.fold_right g na v)) acc tyopt
 
@@ -289,7 +290,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
     f v acc c
-  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc))
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) -> acc))
 
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index c405fcfc72..8670c1d964 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -82,6 +82,7 @@ type 'a glob_constr_r =
   | GSort of glob_sort
   | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
+  | GInt of Uint63.t
 and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
 
 and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index ccbb2934bc..cdeec875a2 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -91,6 +91,7 @@ let kind_of_head env t =
   | Proj (p,c) -> RigidHead RigidOther
 
   | Case (_,_,c,_) -> aux k [] c true
+  | Int _ -> ConstructorHead
   | Fix ((i,j),_) ->
       let n = i.(j) in
       try aux k [] (List.nth l n) true
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index e46d03b743..b5a6ba6be5 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -100,6 +100,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
     let variances = infer_stack infos variances stk in
     infer_vect infos variances (Array.map (mk_clos e) args)
   | FRel _ -> infer_stack infos variances stk
+  | FInt _ -> infer_stack infos variances stk
   | FFlex fl ->
     let variances = infer_table_key infos variances fl in
     infer_stack infos variances stk
@@ -155,6 +156,10 @@ and infer_stack infos variances (stk:CClosure.stack) =
         infer_vect infos variances (Array.map (mk_clos e) br)
       | Zshift _ -> variances
       | Zupdate _ -> variances
+      | Zprimitive (_,_,rargs,kargs) ->
+        let variances = List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances rargs in
+        let variances = List.fold_left (fun variances (_,c) -> infer_fterm CONV infos variances c []) variances kargs in
+        variances
     in
     infer_stack infos variances stk
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index dc2663c1ca..b7090e69da 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -120,13 +120,6 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   let mib,mip = lookup_mind_specif env ind in
   let nparams = mib.mind_nparams in
   let params = Array.sub allargs 0 nparams in
-  try
-    if const then
-      let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
-      Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag, ctyp
-    else
-      raise Not_found
-  with Not_found ->
   let i = invert_tag const tag mip.mind_reloc_tbl in
   let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in
   (mkApp(mkConstructU((ind,i),u), params), ctyp)
@@ -137,7 +130,9 @@ let construct_of_constr const env sigma tag typ =
   match EConstr.kind_upto sigma t with
   | Ind (ind,u) -> 
       construct_of_constr_notnative const env tag ind u l
-  | _ -> assert false
+  | _ ->
+    assert (Constr.equal t (Typeops.type_of_int env));
+    (mkInt (Uint63.of_int tag), t)
 
 let construct_of_constr_const env sigma tag typ =
   fst (construct_of_constr true env sigma tag typ)
@@ -208,6 +203,7 @@ let rec nf_val env sigma v typ =
       let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
       mkLambda(name,dom,body)
   | Vconst n -> construct_of_constr_const env sigma n typ
+  | Vint64 i -> i |> Uint63.of_int64 |> mkInt
   | Vblock b ->
       let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
       let args = nf_bargs env sigma b ctyp in
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index be7ebe49cf..2ca7f21e8d 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -39,6 +39,7 @@ type constr_pattern =
       (int * bool list * constr_pattern) list (** index of constructor, nb of args *)
   | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
   | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
+  | PInt of Uint63.t
 
 (** Nota : in a [PCase], the array of branches might be shorter than
     expected, denoting the use of a final "_ => _" branch *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 248d5d0a0e..6803ea7d9b 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -61,9 +61,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   Int.equal i1 i2 && rec_declaration_eq f1 f2
 | PProj (p1, t1), PProj (p2, t2) ->
    Projection.equal p1 p2 && constr_pattern_eq t1 t2
+| PInt i1, PInt i2 ->
+   Uint63.equal i1 i2
 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
    | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _
-   | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _), _ -> false
+   | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _), _ -> false
 (** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
 
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
@@ -90,7 +92,8 @@ let rec occur_meta_pattern = function
       (occur_meta_pattern c) ||
       (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
   | PMeta _ | PSoApp _ -> true
-  | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
+  | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _
+    | PInt _ -> false
 
 let rec occurn_pattern n = function
   | PRel p -> Int.equal n p
@@ -111,7 +114,7 @@ let rec occurn_pattern n = function
       (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar (_,args) -> Array.exists (occurn_pattern n) args
-  | PVar _ | PRef _ | PSort _ -> false
+  | PVar _ | PRef _ | PSort _ | PInt _ -> false
   | PFix (_,(_,tl,bl)) ->
      Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
   | PCoFix (_,(_,tl,bl)) ->
@@ -134,7 +137,7 @@ let rec head_pattern_bound t =
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PLambda _ -> raise BoundPattern
-    | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
+    | PCoFix _ | PInt _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
 
 let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | Const (sp,_) -> ConstRef sp
@@ -209,7 +212,8 @@ let pattern_of_constr env sigma t =
        let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
        let env' = Array.fold_left2 push env lna tl in
        PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl,
-                  Array.map (pattern_of_constr env') bl)) in
+                  Array.map (pattern_of_constr env') bl))
+    | Int i -> PInt i in
   pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
@@ -231,7 +235,7 @@ let map_pattern_with_binders g f l = function
      let l' = Array.fold_left (fun l na -> g na l) l lna in
      PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
   (* Non recursive *)
-  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x
+  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ | PInt _ as x) -> x
 
 let error_instantiate_pattern id l =
   let is = match l with
@@ -287,7 +291,8 @@ let rec subst_pattern subst pat =
           pattern_of_constr env evd t.Univ.univ_abstracted_value)
   | PVar _
   | PEvar _
-  | PRel _ -> pat
+  | PRel _
+  | PInt _ -> pat
   | PProj (p,c) -> 
       let p' = Projection.map (subst_mind subst) p in
       let c' = subst_pattern subst c in
@@ -488,6 +493,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       let names = Array.map (fun id -> Name id) ids in
       PCoFix (n, (names, tl, cl))
 
+  | GInt i -> PInt i
   | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ ->
       err ?loc (Pp.str "Non supported pattern."))
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c23b20a5d3..57705fa209 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -953,6 +953,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         sigma, { uj_val = v; uj_type = tval }
     in inh_conv_coerce_to_tycon ?loc env sigma cj tycon
 
+      | GInt i ->
+        let resj =
+          try Typing.judge_of_int !!env i
+          with Invalid_argument _ ->
+            user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.")
+        in
+        inh_conv_coerce_to_tycon ?loc env sigma resj tycon
+
 and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
   let f decl (subst,update,sigma) =
     let id = NamedDecl.get_id decl in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 9c9877fd23..98ca329117 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -279,7 +279,9 @@ sig
   | Case of case_info * 'a * 'a array * Cst_stack.t
   | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
+
   and 'a t = 'a member list
 
   exception IncompatibleFold2
@@ -308,6 +310,8 @@ sig
   val nth : 'a t -> int -> 'a
   val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
   val zip : ?refold:bool -> evar_map -> constr * constr t -> constr
+  val check_native_args : CPrimitives.t -> 'a t -> bool
+  val get_next_primitive_args : CPrimitives.args_red -> 'a t -> CPrimitives.args_red * ('a t * 'a * 'a t) option
 end =
 struct
   open EConstr
@@ -336,7 +340,9 @@ struct
   | Case of case_info * 'a * 'a array * Cst_stack.t
   | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
+
   and 'a t = 'a member list
 
   (* Debugging printer *)
@@ -354,6 +360,9 @@ struct
     | Fix (f,args,cst) ->
        str "ZFix(" ++ Constr.debug_print_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
+    | Primitive (p,c,args,kargs,cst_l) ->
+      str "ZPrimitive(" ++ str (CPrimitives.to_string p)
+      ++ pr_comma () ++ pr pr_c args ++ str ")"
     | Cst (mem,curr,remains,params,cst_l) ->
       str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr
       ++ pr_comma () ++
@@ -420,7 +429,7 @@ struct
         equal_cst_member c1 c2
           && equal_rec (List.rev params1) (List.rev params2)
           && equal_rec s1' s2'
-      | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> false
+      | ((App _|Case _|Proj _|Fix _|Cst _|Primitive _)::_|[]), _ -> false
     in equal_rec (List.rev sk1) (List.rev sk2)
 
   let compare_shape stk1 stk2 =
@@ -435,9 +444,11 @@ struct
 	Int.equal bal 0 && compare_rec 0 s1 s2
       | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
+      | (Primitive(_,_,a1,_,_)::s1, Primitive(_,_,a2,_,_)::s2) ->
+        Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
       | (Cst (_,_,_,p1,_)::s1, Cst (_,_,_,p2,_)::s2) ->
-	Int.equal bal 0 && compare_rec 0 p1 p2 && compare_rec 0 s1 s2
-      | (_,_) -> false in
+        Int.equal bal 0 && compare_rec 0 p1 p2 && compare_rec 0 s1 s2
+      | ((Case _|Proj _|Fix _|Cst _|Primitive _) :: _ | []) ,_ -> false in
     compare_rec 0 stk1 stk2
 
   exception IncompatibleFold2
@@ -459,7 +470,7 @@ struct
       | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 ->
         let o' = aux o (List.rev params1) (List.rev params2) in
         aux o' q1 q2
-      | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
+      | (((App _|Case _|Proj _|Fix _|Cst _|Primitive _) :: _|[]), _) ->
               raise IncompatibleFold2
     in aux o (List.rev sk1) (List.rev sk2)
 
@@ -473,7 +484,9 @@ struct
 				  Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg,alt)
 			       | Cst (cst,curr,remains,params,alt) ->
 				 Cst (cst,curr,remains,map f params,alt)
-  ) x
+                               | Primitive (p,c,args,kargs,cst_l) ->
+                                 Primitive(p,c, map f args, kargs, cst_l)
+    ) x
 
   let append_app_list l s =
     let a = Array.of_list l in
@@ -481,7 +494,7 @@ struct
 
   let rec args_size = function
     | App (i,_,j)::s -> j + 1 - i + args_size s
-    | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0
+    | (Case _|Fix _|Proj _|Cst _|Primitive _)::_ | [] -> 0
 
   let strip_app s =
     let rec aux out = function
@@ -504,7 +517,8 @@ struct
     in aux n [] s
 
   let not_purely_applicative args =
-    List.exists (function (Fix _ | Case _ | Proj _ | Cst _) -> true | _ -> false) args
+    List.exists (function (Fix _ | Case _ | Proj _ | Cst _) -> true
+                          | App _ | Primitive _ -> false) args
   let will_expose_iota args =
     List.exists
       (function (Fix (_,_,l) | Case (_,_,_,l) |
@@ -588,9 +602,26 @@ struct
   | f, (Proj (p,cst_l)::s) when refold ->
     zip (best_state sigma (mkProj (p,f),s) cst_l)
   | f, (Proj (p,_)::s) -> zip (mkProj (p,f),s)
+  | f, (Primitive (p,c,args,kargs,cst_l)::s) ->
+      zip (mkConstU c, args @ append_app [|f|] s)
   in
   zip s
 
+  (* Check if there is enough arguments on [stk] w.r.t. arity of [op] *)
+  let check_native_args op stk =
+    let nargs = CPrimitives.arity op in
+    let rargs = args_size stk in
+    nargs <= rargs
+
+  let get_next_primitive_args kargs stk =
+    let rec nargs = function
+      | [] -> 0
+      | CPrimitives.Kwhnf :: _ -> 0
+      | _ :: s -> 1 + nargs s
+    in
+    let n = nargs kargs in
+    (List.skipn (n+1) kargs, strip_n_app n stk)
+
 end
 
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
@@ -815,6 +846,57 @@ let fix_recarg ((recindices,bodynum),_) stack =
   with Not_found ->
     None
 
+open Primred
+
+module CNativeEntries =
+struct
+
+  type elem = EConstr.t
+  type args = EConstr.t array
+  type evd = evar_map
+
+  let get = Array.get
+
+  let get_int evd e =
+    match EConstr.kind evd e with
+    | Int i -> i
+    | _ -> raise Primred.NativeDestKO
+
+  let mkInt env i =
+    mkInt i
+
+  let mkBool env b =
+    let (ct,cf) = get_bool_constructors env in
+    mkConstruct (if b then ct else cf)
+
+    let mkCarry env b e =
+      let int_ty = mkConst @@ get_int_type env in
+      let (c0,c1) = get_carry_constructors env in
+      mkApp (mkConstruct (if b then c1 else c0),[|int_ty;e|])
+
+    let mkIntPair env e1 e2 =
+    let int_ty = mkConst @@ get_int_type env in
+    let c = get_pair_constructor env in
+    mkApp(mkConstruct c, [|int_ty;int_ty;e1;e2|])
+
+  let mkLt env =
+    let (_eq, lt, _gt) = get_cmp_constructors env in
+    mkConstruct lt
+
+  let mkEq env =
+    let (eq, _lt, _gt) = get_cmp_constructors env in
+    mkConstruct eq
+
+  let mkGt env =
+    let (_eq, _lt, gt) = get_cmp_constructors env in
+    mkConstruct gt
+
+end
+
+module CredNative = RedNative(CNativeEntries)
+
+
+
 (** Generic reduction function with environment
 
     Here is where unfolded constant are stored in order to be
@@ -881,47 +963,55 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
          (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack))));
       if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then
        let u' = EInstance.kind sigma u in
-       (match constant_opt_value_in env (c, u') with
-	| None -> fold ()
-	| Some body ->
+       match constant_value_in env (c, u') with
+       | body ->
+         begin
           let body = EConstr.of_constr body in
-	   if not tactic_mode
-	   then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
-		      (body, stack)
-	   else (* Looks for ReductionBehaviour *)
-	     match ReductionBehaviour.get (Globnames.ConstRef c) with
-	     | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
-	     | Some (recargs, nargs, flags) ->
-		if (List.mem `ReductionNeverUnfold flags
-		    || (nargs > 0 && Stack.args_size stack < nargs))
-		then fold ()
-		else (* maybe unfolds *)
-		  if List.mem `ReductionDontExposeCase flags then
-		    let app_sk,sk = Stack.strip_app stack in
-		    let (tm',sk'),cst_l' =
-		      whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
-		    in
-		    let rec is_case x = match EConstr.kind sigma x with
-		      | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
-		      | App (hd, _) -> is_case hd
-		      | Case _ -> true
-		      | _ -> false in
-		    if equal_stacks sigma (x, app_sk) (tm', sk')
-		       || Stack.will_expose_iota sk'
-		       || is_case tm'
-		      then fold ()
-		      else whrec cst_l' (tm', sk' @ sk)
-		  else match recargs with
-		  |[] -> (* if nargs has been specified *)
-			 (* CAUTION : the constant is NEVER refold
-                            (even when it hides a (co)fix) *)
-		    whrec cst_l (body, stack)
-		  |curr::remains -> match Stack.strip_n_app curr stack with
-		    | None -> fold ()
-		    | Some (bef,arg,s') ->
-		      whrec Cst_stack.empty 
-			(arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
-       ) else fold ()
+          if not tactic_mode
+          then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
+              (body, stack)
+          else (* Looks for ReductionBehaviour *)
+            match ReductionBehaviour.get (Globnames.ConstRef c) with
+            | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
+            | Some (recargs, nargs, flags) ->
+              if (List.mem `ReductionNeverUnfold flags
+                  || (nargs > 0 && Stack.args_size stack < nargs))
+              then fold ()
+              else (* maybe unfolds *)
+              if List.mem `ReductionDontExposeCase flags then
+                let app_sk,sk = Stack.strip_app stack in
+                let (tm',sk'),cst_l' =
+                  whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
+                in
+                let rec is_case x = match EConstr.kind sigma x with
+                  | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+                  | App (hd, _) -> is_case hd
+                  | Case _ -> true
+                  | _ -> false in
+                if equal_stacks sigma (x, app_sk) (tm', sk')
+                || Stack.will_expose_iota sk'
+                || is_case tm'
+                then fold ()
+                else whrec cst_l' (tm', sk' @ sk)
+              else match recargs with
+                |[] -> (* if nargs has been specified *)
+                  (* CAUTION : the constant is NEVER refold
+                                          (even when it hides a (co)fix) *)
+                  whrec cst_l (body, stack)
+                |curr::remains -> match Stack.strip_n_app curr stack with
+                              | None -> fold ()
+                              | Some (bef,arg,s') ->
+                                whrec Cst_stack.empty
+                                        (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
+         end
+       | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack ->
+          let kargs = CPrimitives.kind p in
+          let (kargs,o) = Stack.get_next_primitive_args kargs stack in
+          (* Should not fail thanks to [check_native_args] *)
+          let (before,a,after) = Option.get o in
+          whrec Cst_stack.empty (a,Stack.Primitive(p,const,before,kargs,cst_l)::after)
+       | exception NotEvaluableConst _ -> fold ()
+      else fold ()
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
       (let npars = Projection.npars p in
          if not tactic_mode then
@@ -1049,6 +1139,30 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	|_ -> fold ()
       else fold ()
 
+    | Int i ->
+      begin match Stack.strip_app stack with
+       | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) ->
+         let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in
+         if more_to_reduce then
+           let (kargs,o) = Stack.get_next_primitive_args kargs s in
+           (* Should not fail because Primitive is put on the stack only if fully applied *)
+           let (before,a,after) = Option.get o in
+           whrec Cst_stack.empty (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs,cst_l')::after)
+         else
+           let n = List.length kargs in
+           let (args,s) = Stack.strip_app s in
+           let (args,extra_args) =
+             try List.chop n args
+             with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *)
+           in
+           let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in
+             begin match CredNative.red_prim env sigma p args with
+               | Some t -> whrec cst_l' (t,s)
+               | None -> ((mkApp (mkConstU kn, args), s), cst_l)
+             end
+       | _ -> fold ()
+      end
+
     | Rel _ | Var _ | LetIn _ | Proj _ -> fold ()
     | Sort _ | Ind _ | Prod _ -> fold ()
   in
@@ -1127,7 +1241,8 @@ let local_whd_state_gen flags sigma =
 	|_ -> s
       else s
 
-    | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _  | Ind _ | Proj _ -> s
+    | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _  | Ind _ | Proj _
+      | Int _ -> s
 
   in
   whrec
@@ -1577,7 +1692,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 	if isConstruct sigma t_o then
           whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'')
 	else s,csts'
-      |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts'
+      |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s,csts'
   in whrec csts s
 
 let find_conclusion env sigma =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index a1fd610676..fae0b23b83 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -77,6 +77,7 @@ module Stack : sig
   | Case of case_info * 'a * 'a array * Cst_stack.t
   | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
   | Cst of cst_member
            * int (* current foccussed arg *)
            * int list (* remaining args *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 62ad296ecb..a76a203e37 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -143,6 +143,7 @@ let retype ?(polyprop=true) sigma =
 	 with Invalid_argument _ -> retype_error BadRecursiveType)
     | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
+    | Int _ -> EConstr.of_constr (Typeops.type_of_int env)
 
   and sort_of env t =
     match EConstr.kind sigma t with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2e7176a6b3..2308a541fb 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -48,8 +48,8 @@ let error_not_evaluable r =
      spc () ++ str "to an evaluable reference.")
 
 let is_evaluable_const env cst =
-  is_transparent env (ConstKey cst) && 
-  evaluable_constant cst env
+  is_transparent env (ConstKey cst) &&
+    (evaluable_constant cst env || is_primitive env cst)
 
 let is_evaluable_var env id =
   is_transparent env (VarKey id) && evaluable_named id env
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b5729d7574..e8d935fcbb 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -306,6 +306,9 @@ let type_of_constructor env sigma ((ind,_ as ctor),u) =
   let sigma = Evd.add_constraints sigma csts in
   sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
 
+let judge_of_int env v =
+  Termops.on_judgment EConstr.of_constr (judge_of_int env v)
+
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env sigma cstr =
@@ -408,6 +411,9 @@ let rec execute env sigma cstr =
         let sigma, tj = type_judgment env sigma tj in
         judge_of_cast env sigma cj k tj
 
+    | Int i ->
+        sigma, judge_of_int env i
+
 and execute_recdef env sigma (names,lar,vdef) =
   let sigma, larj = execute_array env sigma lar in
   let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 79f2941554..1ea16bbf34 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -55,3 +55,4 @@ val judge_of_abstraction : Environ.env -> Name.t ->
 val judge_of_product : Environ.env -> Name.t ->
   unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
 val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment
+val judge_of_int : Environ.env -> Uint63.t -> unsafe_judgment
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f0cd5c5f6a..e4d96da0a6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -550,7 +550,7 @@ let is_rigid_head sigma flags t =
   match EConstr.kind sigma t with
   | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst)
   | Ind (i,u) -> true
-  | Construct _ -> true
+  | Construct _ | Int _ -> true
   | Fix _ | CoFix _ -> true
   | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod (_, _, _)
     | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _)
@@ -641,7 +641,7 @@ let rec is_neutral env sigma ts t =
     | Evar _ | Meta _ -> true
     | Case (_, p, c, cl) -> is_neutral env sigma ts c
     | Proj (p, c) -> is_neutral env sigma ts c
-    | Lambda _ | LetIn _ | Construct _ | CoFix _ -> false
+    | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ -> false
     | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
     | Fix _ -> false (* This is an approximation *)
     | App _ -> assert false
@@ -1799,7 +1799,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 
           | Cast (_, _, _) (* Is this expected? *)
           | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
-            | Construct _ -> user_err Pp.(str "Match_subterm")))
+            | Construct _ | Int _ -> user_err Pp.(str "Match_subterm")))
   in
   try matchrec cl
   with ex when precatchable_exception ex ->
@@ -1868,7 +1868,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
           | Cast (_, _, _)  -> fail "Match_subterm" (* Is this expected? *)
 
           | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
-            | Construct _ -> fail "Match_subterm"))
+            | Construct _ | Int _ -> fail "Match_subterm"))
 
   in
   let res = matchrec cl [] in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 113aac25da..083661a64b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -57,7 +57,7 @@ let find_rectype_a env c =
   let (t, l) = decompose_appvect (whd_all env c) in
   match kind t with
   | Ind ind -> (ind, l)
-  | _ -> assert false
+  | _ -> raise Not_found
 
 (* Instantiate inductives and parameters in constructor type *)
 
@@ -75,25 +75,18 @@ let type_constructor mind mib u typ params =
 
 
 let construct_of_constr const env tag typ =
-  let ((mind,_ as ind), u) as indu, allargs = find_rectype_a env typ in
-  (* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
-  try
-    if const then
-      ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag),
-       typ) (*spiwack: this may need to be changed in case there are parameters in the
-	               type which may cause a constant value to have an arity.
-	               (type_constructor seems to be all about parameters actually)
-	               but it shouldn't really matter since constant values don't use
-	               their ctyp in the rest of the code.*)
-    else
-      raise Not_found (* No retroknowledge function (yet) for block decompilation *)
-  with Not_found ->
+  let (t, allargs) = decompose_appvect (whd_all env typ) in
+  match Constr.kind t with
+  | Ind ((mind,_ as ind), u as indu) ->
     let mib,mip = lookup_mind_specif env ind in
     let nparams = mib.mind_nparams in
     let i = invert_tag const tag mip.mind_reloc_tbl in
     let params = Array.sub allargs 0 nparams in
     let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in
-      (mkApp(mkConstructUi(indu,i), params), ctyp)
+    (mkApp(mkConstructUi(indu,i), params), ctyp)
+  | _ ->
+     assert (Constr.equal t (Typeops.type_of_int env));
+      (mkInt (Uint63.of_int tag), t)
 
 let construct_of_constr_const env tag typ =
   fst (construct_of_constr true env tag typ)
@@ -169,6 +162,7 @@ and nf_whd env sigma whd typ =
       let capp,ctyp = construct_of_constr_block env tag typ in
       let args = nf_bargs env sigma b ofs ctyp in
       mkApp(capp,args)
+  | Vint64 i -> i |> Uint63.of_int64 |> mkInt
   | Vatom_stk(Aid idkey, stk) ->
       constr_type_of_idkey env sigma idkey stk
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->
@@ -344,9 +338,9 @@ and nf_fun env sigma f typ =
   let name,dom,codom =
     try decompose_prod env typ
     with DestKO ->
-      (* 27/2/13: Turned this into an anomaly *)
       CErrors.anomaly
-        (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+        Pp.(strbrk "Returned a functional value in type " ++
+            Termops.Internal.print_constr_env env sigma (EConstr.of_constr typ))
   in
   let body = nf_val (push_rel (LocalAssum (name,dom)) env) sigma vb codom in
   mkLambda(name,dom,body)