Primitive integers

This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.

Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.

This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.

Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

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 517834f014..cc9de0c440 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 ace2868255..fd91a17a9a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -954,6 +954,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)