Support for evars and metas in native compiler.

Experimental. Turned out to be much harder to implement than I thought. The main
issue is that the reification in the native compiler and the VM is not quite
untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence,
when reifying an application u = t a1 ... an, the type of t has to be known or
reconstructed. It is always possible to do so in plain CIC, when u is in normal
form and its type is known. However, with partial terms this may no longer be
the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of
evars and metas.

This still has to be tested more extensively, but the correction of the kernel
native conversion (on terms without evars or metas) should not be impacted.

Much of this could be reused for the VM.

16 files changed, 252 insertions, 117 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 1d560e699..9cb46978a 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -104,6 +104,7 @@ Glob_ops
 Redops
 Reductionops
 Inductiveops
+Nativenorm
 Retyping
 Cbv
 Pretype_errors
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 4e34cd60f..7d542c107 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -130,6 +130,8 @@ type symbol =
   | SymbConst of constant
   | SymbMatch of annot_sw
   | SymbInd of inductive
+  | SymbMeta of metavariable
+  | SymbEvar of existential
 
 let dummy_symb = SymbValue (dummy_value ())
 
@@ -141,6 +143,9 @@ let eq_symbol sy1 sy2 =
   | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2
   | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2
   | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2
+  | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
+  | SymbEvar (evk1,args1), SymbEvar (evk2,args2) ->
+     Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2
   | _, _ -> false
 
 open Hashset.Combine
@@ -153,6 +158,11 @@ let hash_symbol symb =
   | SymbConst c -> combinesmall 4 (Constant.hash c)
   | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
   | SymbInd ind -> combinesmall 6 (ind_hash ind)
+  | SymbMeta m -> combinesmall 7 m
+  | SymbEvar (evk,args) ->
+     let evh = Evar.hash evk in
+     let hl = Array.fold_left (fun h t -> combine h (Constr.hash t)) evh args in
+     combinesmall 8 hl
 
 module HashedTypeSymbol = struct
   type t = symbol
@@ -196,6 +206,16 @@ let get_ind tbl i =
     | SymbInd ind -> ind
     | _ -> anomaly (Pp.str "get_ind failed")
 
+let get_meta tbl i =
+  match tbl.(i) with
+    | SymbMeta m -> m
+    | _ -> anomaly (Pp.str "get_meta failed")
+
+let get_evar tbl i =
+  match tbl.(i) with
+    | SymbEvar ev -> ev
+    | _ -> anomaly (Pp.str "get_evar failed")
+
 let push_symbol x =
   try HashtblSymbol.find symb_tbl x
   with Not_found ->
@@ -209,7 +229,7 @@ let get_symbols_tbl () =
   HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl(**}}}**)
 
 (** Lambda to Mllambda {{{**)
-  
+
 type primitive =
   | Mk_prod
   | Mk_sort
@@ -224,6 +244,8 @@ type primitive =
   | Cast_accu
   | Upd_cofix
   | Force_cofix
+  | Mk_meta
+  | Mk_evar
 
 let eq_primitive p1 p2 =
   match p1, p2 with
@@ -240,6 +262,8 @@ let eq_primitive p1 p2 =
   | Cast_accu, Cast_accu -> true
   | Upd_cofix, Upd_cofix -> true
   | Force_cofix, Force_cofix -> true
+  | Mk_meta, Mk_meta -> true
+  | Mk_evar, Mk_evar -> true
   | _ -> false
 
 type mllambda =
@@ -709,6 +733,12 @@ let get_match_code i =
 let get_ind_code i =
   MLapp (MLglobal (Ginternal "get_ind"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
 
+let get_meta_code i =
+  MLapp (MLglobal (Ginternal "get_meta"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
+let get_evar_code i =
+  MLapp (MLglobal (Ginternal "get_evar"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
 type rlist =
   | Rnil 
   | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' 
@@ -745,6 +775,15 @@ let merge_branches t =
   match t with
   | Lrel(id ,i) -> get_rel env id i
   | Lvar id -> get_var env id
+  | Lmeta(mv,ty) ->
+     let tyn = fresh_lname Anonymous in
+     let i = push_symbol (SymbMeta mv) in
+     MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|])
+  | Levar(ev,ty) ->
+     let tyn = fresh_lname Anonymous in
+     let i = push_symbol (SymbEvar ev) in
+     MLlet(tyn, ml_of_lam env l ty,
+       MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn|]))
   | Lprod(dom,codom) ->
       let dom = ml_of_lam env l dom in
       let codom = ml_of_lam env l codom in
@@ -1299,7 +1338,7 @@ let pp_mllam fmt l =
 
   and pp_blam fmt l =
     match l with
-    | MLprimitive (Mk_prod | Mk_sort) 
+    | MLprimitive (Mk_prod | Mk_sort) (* FIXME: why this special case? *)
     | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
 	Format.fprintf fmt "(%a)" pp_mllam l
     | MLconstruct(_,_,args) when Array.length args > 0 ->
@@ -1314,7 +1353,7 @@ let pp_mllam fmt l =
       for i = 1 to len - 1 do
 	Format.fprintf fmt "%s%a" sep pp_blam args.(i)
       done
-    end 
+    end
 
   and pp_cargs fmt args =
     let len = Array.length args in
@@ -1378,6 +1417,8 @@ let pp_mllam fmt l =
     | Cast_accu -> Format.fprintf fmt "cast_accu"
     | Upd_cofix -> Format.fprintf fmt "upd_cofix"
     | Force_cofix -> Format.fprintf fmt "force_cofix"
+    | Mk_meta -> Format.fprintf fmt "mk_meta_accu"
+    | Mk_evar -> Format.fprintf fmt "mk_evar_accu"
   in
   Format.fprintf fmt "@[%a@]" pp_mllam l
   
@@ -1428,18 +1469,18 @@ let pp_global fmt g =
       Format.fprintf fmt "@[(* %s *)@]@." s(**}}}**)
 
 (** Compilation of elements in environment {{{**)
-let rec compile_with_fv env auxdefs l t =
+let rec compile_with_fv env sigma auxdefs l t =
   let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
   if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml)
-  else apply_fv env (fv_named,fv_rel) auxdefs ml
+  else apply_fv env sigma (fv_named,fv_rel) auxdefs ml
 
-and apply_fv env (fv_named,fv_rel) auxdefs ml =
+and apply_fv env sigma (fv_named,fv_rel) auxdefs ml =
   let get_rel_val (n,_) auxdefs =
     (*
     match !(lookup_rel_native_val n env) with
     | NVKnone ->
     *)
-        compile_rel env auxdefs n
+        compile_rel env sigma auxdefs n
 (*    | NVKvalue (v,d) -> assert false *)
   in
   let get_named_val (id,_) auxdefs =
@@ -1447,7 +1488,7 @@ and apply_fv env (fv_named,fv_rel) auxdefs ml =
     match !(lookup_named_native_val id env) with
     | NVKnone ->
         *)
-        compile_named env auxdefs id
+        compile_named env sigma auxdefs id
 (*    | NVKvalue (v,d) -> assert false *)
   in
   let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
@@ -1458,32 +1499,32 @@ and apply_fv env (fv_named,fv_rel) auxdefs ml =
   let aux_name = fresh_lname Anonymous in
   auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
 
-and compile_rel env auxdefs n =
+and compile_rel env sigma auxdefs n =
   let (_,body,_) = lookup_rel n env.env_rel_context in
   let n = rel_context_length env.env_rel_context - n in
   match body with
   | Some t ->
-      let code = lambda_of_constr env t in
-      let auxdefs,code = compile_with_fv env auxdefs None code in
+      let code = lambda_of_constr env sigma t in
+      let auxdefs,code = compile_with_fv env sigma auxdefs None code in
       Glet(Grel n, code)::auxdefs
   | None -> 
       Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
 
-and compile_named env auxdefs id =
+and compile_named env sigma auxdefs id =
   let (_,body,_) = lookup_named id env.env_named_context in
   match body with
   | Some t ->
-      let code = lambda_of_constr env t in
-      let auxdefs,code = compile_with_fv env auxdefs None code in
+      let code = lambda_of_constr env sigma t in
+      let auxdefs,code = compile_with_fv env sigma auxdefs None code in
       Glet(Gnamed id, code)::auxdefs
   | None -> 
       Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
 
-let compile_constant env prefix ~interactive con body =
+let compile_constant env sigma prefix ~interactive con body =
   match body with
   | Def t ->
       let t = Lazyconstr.force t in
-      let code = lambda_of_constr env t in
+      let code = lambda_of_constr env sigma t in
       let is_lazy = is_lazy t in
       let code = if is_lazy then mk_lazy code else code in
       let name =
@@ -1491,7 +1532,7 @@ let compile_constant env prefix ~interactive con body =
         else Linked prefix
       in
       let l = con_label con in
-      let auxdefs,code = compile_with_fv env [] (Some l) code in
+      let auxdefs,code = compile_with_fv env sigma [] (Some l) code in
       let code =
         optimize_stk (Glet(Gconstant ("",con),code)::auxdefs)
       in
@@ -1574,10 +1615,8 @@ let compile_mind_deps env prefix ~interactive
 
 (* This function compiles all necessary dependencies of t, and generates code in
    reverse order, as well as linking information updates *)
-let rec compile_deps env prefix ~interactive init t =
+let rec compile_deps env sigma prefix ~interactive init t =
   match kind_of_term t with
-  | Meta _ -> invalid_arg "Nativecode.compile_deps: Meta"
-  | Evar _ -> invalid_arg "Nativecode.compile_deps: Evar"
   | Ind (mind,_) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
       let c = get_allias env c in
@@ -1588,10 +1627,13 @@ let rec compile_deps env prefix ~interactive init t =
       then init
       else
       let comp_stack, (mind_updates, const_updates) = match cb.const_body with
-        | Def t -> compile_deps env prefix ~interactive init (Lazyconstr.force t)
+        | Def t ->
+	   compile_deps env sigma prefix ~interactive init (Lazyconstr.force t)
         | _ -> init
       in
-      let code, name = compile_constant env prefix ~interactive c cb.const_body in
+      let code, name =
+	compile_constant env sigma prefix ~interactive c cb.const_body
+      in
       let comp_stack = code@comp_stack in
       let const_updates = Cmap_env.add c (nameref, name) const_updates in
       comp_stack, (mind_updates, const_updates)
@@ -1599,12 +1641,13 @@ let rec compile_deps env prefix ~interactive init t =
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
-      fold_constr (compile_deps env prefix ~interactive) init t
-  | _ -> fold_constr (compile_deps env prefix ~interactive) init t
+      fold_constr (compile_deps env sigma prefix ~interactive) init t
+  | _ -> fold_constr (compile_deps env sigma prefix ~interactive) init t
 
 let compile_constant_field env prefix con acc cb =
     let (gl, _) =
-      compile_constant ~interactive:false env prefix con cb.const_body
+      compile_constant ~interactive:false env empty_evars prefix
+        con cb.const_body
     in
     gl@acc
 
@@ -1618,19 +1661,19 @@ let mk_internal_let s code =
   Glet(Ginternal s, code)
 
 (* ML Code for conversion function *)
-let mk_conv_code env prefix t1 t2 =
+let mk_conv_code env sigma prefix t1 t2 =
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
-    compile_deps env prefix ~interactive:true init t1
+    compile_deps env sigma prefix ~interactive:true init t1
   in
   let gl, (mind_updates, const_updates) =
     let init = (gl, (mind_updates, const_updates)) in
-    compile_deps env prefix ~interactive:true init t2
+    compile_deps env sigma prefix ~interactive:true init t2
   in
-  let code1 = lambda_of_constr env t1 in
-  let code2 = lambda_of_constr env t2 in
-  let (gl,code1) = compile_with_fv env gl None code1 in
-  let (gl,code2) = compile_with_fv env gl None code2 in
+  let code1 = lambda_of_constr env sigma t1 in
+  let code2 = lambda_of_constr env sigma t2 in
+  let (gl,code1) = compile_with_fv env sigma gl None code1 in
+  let (gl,code2) = compile_with_fv env sigma gl None code2 in
   let t1 = mk_internal_let "t1" code1 in
   let t2 = mk_internal_let "t2" code2 in
   let g1 = MLglobal (Ginternal "t1") in
@@ -1643,13 +1686,13 @@ let mk_conv_code env prefix t1 t2 =
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
-let mk_norm_code env prefix t =
+let mk_norm_code env sigma prefix t =
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
-    compile_deps env prefix ~interactive:true init t
+    compile_deps env sigma prefix ~interactive:true init t
   in
-  let code = lambda_of_constr env t in
-  let (gl,code) = compile_with_fv env gl None code in
+  let code = lambda_of_constr env sigma t in
+  let (gl,code) = compile_with_fv env sigma gl None code in
   let t1 = mk_internal_let "t1" code in
   let g1 = MLglobal (Ginternal "t1") in
   let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index f6a0c79f4..7e7094963 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -38,6 +38,10 @@ val get_match : symbol array -> int -> Nativevalues.annot_sw
 
 val get_ind : symbol array -> int -> inductive
 
+val get_meta : symbol array -> int -> metavariable
+
+val get_evar : symbol array -> int -> existential
+
 val get_symbols_tbl : unit -> symbol array
 
 type code_location_update
@@ -56,8 +60,8 @@ val compile_constant_field : env -> string -> constant ->
 val compile_mind_field : string -> module_path -> label ->
   global list -> mutual_inductive_body -> global list
 
-val mk_conv_code : env -> string -> constr -> constr -> linkable_code
-val mk_norm_code : env -> string -> constr -> linkable_code
+val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code
+val mk_norm_code : env -> evars -> string -> constr -> linkable_code
 
 val mk_library_header : dir_path -> global list
 
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 14b55e91a..3435e1d75 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -127,7 +127,7 @@ and conv_fix lvl t1 f1 t2 f2 cu =
     else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in
   aux 0 cu
 
-let native_conv pb env t1 t2 =
+let native_conv pb sigma env t1 t2 =
   if !Flags.no_native_compiler then begin
     let msg = "Native compiler is disabled, "^
     "falling back to VM conversion test." in
@@ -137,7 +137,7 @@ let native_conv pb env t1 t2 =
   else
   let env = Environ.pre_env env in 
   let ml_filename, prefix = get_ml_filename () in
-  let code, upds = mk_conv_code env prefix t1 t2 in
+  let code, upds = mk_conv_code env sigma prefix t1 t2 in
   match compile ml_filename code with
   | (0,fn) ->
       begin
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 2cb5ac797..248130076 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -9,7 +9,8 @@ open Term
 open Univ
 open Environ
 open Reduction
+open Nativelambda
 
 (** This module implements the conversion test by compiling to OCaml code *)
 
-val native_conv : conv_pb -> types conversion_function
+val native_conv : conv_pb -> evars -> types conversion_function
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 800c8e5fb..258f03efd 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -17,6 +17,8 @@ open Nativevalues
 type lambda =
   | Lrel          of name * int 
   | Lvar          of identifier
+  | Lmeta         of metavariable * lambda (* type *)
+  | Levar         of existential * lambda (* type *)
   | Lprod         of lambda * lambda 
   | Llam          of name array * lambda  
   | Llet          of name * lambda * lambda
@@ -41,23 +43,28 @@ type lambda =
 and lam_branches = (constructor * name array * lambda) array 
       
 and fix_decl =  name array * lambda array * lambda array
-      
+
+type evars =
+    { evars_val : existential -> constr option;
+      evars_typ : existential -> types;
+      evars_metas : metavariable -> types }
+
 (*s Constructors *)
-  
+
 let mkLapp f args =
   if Array.is_empty args then f
   else
     match f with
     | Lapp(f', args') -> Lapp (f', Array.append args' args)
     | _ -> Lapp(f, args)
-	  
+
 let mkLlam ids body =
   if Array.is_empty ids then body
   else 
     match body with
     | Llam(ids', body) -> Llam(Array.append ids ids', body)
     | _ -> Llam(ids, body)
-  
+
 let decompose_Llam lam =
   match lam with
   | Llam(ids,body) -> ids, body
@@ -103,8 +110,8 @@ let get_const_prefix env c =
 
 let map_lam_with_binders g f n lam =
   match lam with
-  | Lrel _ | Lvar _  | Lconst _ | Lval _
-  | Lsort _ | Lind _ | Lconstruct _ | Llazy | Lforce -> lam
+  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lconstruct _
+  | Llazy | Lforce | Lmeta _ | Levar _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -199,8 +206,8 @@ let lam_subst_args subst args =
   
 let can_subst lam = 
   match lam with
-  | Lrel _ | Lvar _ | Lconst _
-  | Lval _ | Lsort _ | Lind _ | Llam _ | Lconstruct _ -> true
+  | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Llam _
+  | Lconstruct _ | Lmeta _ | Levar _ -> true
   | _ -> false
 
 let can_merge_if bt bf =
@@ -307,7 +314,7 @@ let rec occurence k kind lam =
 	if kind then false else raise Not_found
       else kind
   | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _
-  | Lconstruct _ | Llazy | Lforce -> kind
+  | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
   | Lprod(dom, codom) ->
       occurence k (occurence k kind dom) codom
   | Llam(ids,body) ->
@@ -509,29 +516,48 @@ module Renv =
 let is_lazy t = (* APPROXIMATION *)
   isApp t || isLetIn t
 
+let evar_value sigma ev = sigma.evars_val ev
+
+let evar_type sigma ev = sigma.evars_typ ev
+
+let meta_type sigma mv = sigma.evars_metas mv
+
+let empty_evars =
+  { evars_val = (fun _ -> None);
+    evars_typ = (fun _ -> assert false);
+    evars_metas = (fun _ -> assert false) }
+
 let empty_ids = [||]
 
-let rec lambda_of_constr env c =
-(*  try *)
+let rec lambda_of_constr env sigma c =
   match kind_of_term c with
-  | Meta _ -> invalid_arg "Nativelambda.lambda_of_constr: Meta"
-  | Evar _ -> invalid_arg "Nativelambda.lambda_of_constr : Evar"
+  | Meta mv ->
+     let ty = meta_type sigma mv in
+     Lmeta (mv, lambda_of_constr env sigma ty)
 
-  | Cast (c, _, _) -> lambda_of_constr env c
+  | Evar ev ->
+     (match evar_value sigma ev with
+     | None ->
+	let ty = evar_type sigma ev in
+	Levar(ev, lambda_of_constr env sigma ty)
+     | Some t -> lambda_of_constr env sigma t)
+
+  | Cast (c, _, _) -> lambda_of_constr env sigma c
 
   | Rel i -> Renv.get env i
 
   | Var id -> Lvar id
 
   | Sort s -> Lsort s
+
   | Ind ind ->
       let prefix = get_mind_prefix !global_env (fst ind) in
       Lind (prefix, ind)
-	
+
   | Prod(id, dom, codom) ->
-      let ld = lambda_of_constr env dom in
+      let ld = lambda_of_constr env sigma dom in
       Renv.push_rel env id;
-      let lc = lambda_of_constr env codom in
+      let lc = lambda_of_constr env sigma codom in
       Renv.pop env;
       Lprod(ld,  Llam([|id|], lc))
 
@@ -539,22 +565,22 @@ let rec lambda_of_constr env c =
       let params, body = decompose_lam c in
       let ids = get_names (List.rev params) in
       Renv.push_rels env ids;
-      let lb = lambda_of_constr env body in
+      let lb = lambda_of_constr env sigma body in
       Renv.popn env (Array.length ids);
       mkLlam ids lb
 
   | LetIn(id, def, _, body) ->
-      let ld = lambda_of_constr env def in
+      let ld = lambda_of_constr env sigma def in
       Renv.push_rel env id;
-      let lb = lambda_of_constr env body in
+      let lb = lambda_of_constr env sigma body in
       Renv.pop env;
       Llet(id, ld, lb)
 
-  | App(f, args) -> lambda_of_app env f args
+  | App(f, args) -> lambda_of_app env sigma f args
 
-  | Const _ -> lambda_of_app env c empty_args
+  | Const _ -> lambda_of_app env sigma c empty_args
 
-  | Construct _ ->  lambda_of_app env c empty_args
+  | Construct _ ->  lambda_of_app env sigma c empty_args
 
   | Case(ci,t,a,branches) ->  
       let (mind,i as ind) = ci.ci_ind in
@@ -571,14 +597,14 @@ let rec lambda_of_constr env c =
           asw_prefix = prefix}
       in
       (* translation of the argument *)
-      let la = lambda_of_constr env a in
+      let la = lambda_of_constr env sigma a in
       (* translation of the type *)
-      let lt = lambda_of_constr env t in
+      let lt = lambda_of_constr env sigma t in
       (* translation of branches *)
       let mk_branch i b =
 	let cn = (ind,i+1) in
 	let _, arity = tbl.(i) in
-	let b = lambda_of_constr env b in
+	let b = lambda_of_constr env sigma b in
 	if Int.equal arity 0 then (cn, empty_ids, b)
 	else 
 	  match b with
@@ -592,20 +618,20 @@ let rec lambda_of_constr env c =
       Lcase(annot_sw, lt, la, bs)
 	
   | Fix(rec_init,(names,type_bodies,rec_bodies)) ->
-      let ltypes = lambda_of_args env 0 type_bodies in
+      let ltypes = lambda_of_args env sigma 0 type_bodies in
       Renv.push_rels env names;
-      let lbodies = lambda_of_args env 0 rec_bodies in
+      let lbodies = lambda_of_args env sigma 0 rec_bodies in
       Renv.popn env (Array.length names);
       Lfix(rec_init, (names, ltypes, lbodies))
 	
   | CoFix(init,(names,type_bodies,rec_bodies)) ->
-      let ltypes = lambda_of_args env 0 type_bodies in 
+      let ltypes = lambda_of_args env sigma 0 type_bodies in 
       Renv.push_rels env names;
-      let lbodies = lambda_of_args env 0 rec_bodies in
+      let lbodies = lambda_of_args env sigma 0 rec_bodies in
       Renv.popn env (Array.length names);
       Lcofix(init, (names, ltypes, lbodies))
 
-and lambda_of_app env f args =
+and lambda_of_app env sigma f args =
   match kind_of_term f with
   | Const kn ->
       let kn = get_allias !global_env kn in
@@ -613,7 +639,7 @@ and lambda_of_app env f args =
       begin match cb.const_body with
       | Def csubst ->
           if cb.const_inline_code then
-            lambda_of_app env (Lazyconstr.force csubst) args
+            lambda_of_app env sigma (Lazyconstr.force csubst) args
           else
           let prefix = get_const_prefix !global_env kn in
           let t =
@@ -621,31 +647,31 @@ and lambda_of_app env f args =
               mkLapp Lforce [|Lconst (prefix, kn)|]
             else Lconst (prefix, kn)
           in
-        mkLapp t (lambda_of_args env 0 args)
+        mkLapp t (lambda_of_args env sigma 0 args)
       | OpaqueDef _ | Undef _ ->
           let prefix = get_const_prefix !global_env kn in
-          mkLapp (Lconst (prefix, kn)) (lambda_of_args env 0 args)
+          mkLapp (Lconst (prefix, kn)) (lambda_of_args env sigma 0 args)
       end
   | Construct c ->
       let tag, nparams, arity = Renv.get_construct_info env c in
       let expected = nparams + arity in
       let nargs = Array.length args in
       if Int.equal nargs expected then 
-	let args = lambda_of_args env nparams args in
+	let args = lambda_of_args env sigma nparams args in
 	makeblock !global_env c tag args
       else
         let prefix = get_mind_prefix !global_env (fst (fst c)) in
-        mkLapp (Lconstruct (prefix, c)) (lambda_of_args env 0 args)
+        mkLapp (Lconstruct (prefix, c)) (lambda_of_args env sigma 0 args)
   | _ -> 
-      let f = lambda_of_constr env f in
-      let args = lambda_of_args env 0 args in
+      let f = lambda_of_constr env sigma f in
+      let args = lambda_of_args env sigma 0 args in
       mkLapp f args
 	
-and lambda_of_args env start args =
+and lambda_of_args env sigma start args =
   let nargs = Array.length args in
   if start < nargs then
     Array.init (nargs - start) 
-      (fun i -> lambda_of_constr env args.(start + i))
+      (fun i -> lambda_of_constr env sigma args.(start + i))
   else empty_args
 
 let optimize lam =
@@ -657,12 +683,12 @@ let optimize lam =
     (msgerrnl (str "Remove let = \n" ++ pp_lam lam);flush_all()); *)
   lam
 
-let lambda_of_constr env c =
+let lambda_of_constr env sigma c =
   set_global_env env;
   let env = Renv.make () in
   let ids = List.rev_map (fun (id, _, _) -> id) !global_env.env_rel_context in
   Renv.push_rels env (Array.of_list ids);
-  let lam = lambda_of_constr env c in
+  let lam = lambda_of_constr env sigma c in
 (*  if Flags.vm_draw_opt () then begin
     (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all()); 
     (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all()); 
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 997efd969..860283e06 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -18,6 +18,8 @@ open Nativevalues
 type lambda =
   | Lrel          of name * int 
   | Lvar          of identifier
+  | Lmeta         of metavariable * lambda (* type *)
+  | Levar         of existential * lambda (* type *)
   | Lprod         of lambda * lambda 
   | Llam          of name array * lambda  
   | Llet          of name * lambda * lambda
@@ -40,9 +42,16 @@ type lambda =
   | Lforce
 
 and lam_branches = (constructor * name array * lambda) array 
-      
+
 and fix_decl =  name array * lambda array * lambda array
 
+type evars =
+    { evars_val : existential -> constr option;
+      evars_typ : existential -> types;
+      evars_metas : metavariable -> types }
+
+val empty_evars : evars
+
 val decompose_Llam : lambda -> Names.name array * lambda
 val decompose_Llam_Llet : lambda -> (Names.name * lambda option) array * lambda
 
@@ -51,4 +60,4 @@ val mk_lazy : lambda -> lambda
 
 val get_allias : env -> constant -> constant
 
-val lambda_of_constr : env -> types -> lambda
+val lambda_of_constr : env -> evars -> Constr.constr -> lambda
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index c38b72031..c3e2b3ab7 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -58,6 +58,8 @@ type atom =
   | Acofix of t array * t array * int * t
   | Acofixe of t array * t array * int * t
   | Aprod of name * t * (t -> t)
+  | Ameta of metavariable * t
+  | Aevar of existential * t
 
 let accumulate_tag = 0
 
@@ -120,6 +122,12 @@ let mk_sw_accu annot c p ac =
 let mk_prod_accu s dom codom =
   mk_accu (Aprod (s,dom,codom))
 
+let mk_meta_accu mv ty =
+  mk_accu (Ameta (mv,ty))
+
+let mk_evar_accu ev ty =
+  mk_accu (Aevar (ev,ty))
+
 let atom_of_accu (k:accumulator) =
   (Obj.magic (Obj.field (Obj.magic k) 2) : atom)
 
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index c8adb07e5..150811b72 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -50,6 +50,8 @@ type atom =
   | Acofix of t array * t array * int * t
   | Acofixe of t array * t array * int * t
   | Aprod of name * t * (t -> t)
+  | Ameta of metavariable * t
+  | Aevar of existential * t
 
 (* Constructors *)
 
@@ -63,7 +65,9 @@ val mk_var_accu : identifier -> t
 val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
 val mk_prod_accu : name -> t -> t -> t
 val mk_fix_accu : rec_pos  -> int -> t array -> t array -> t
-val mk_cofix_accu : int -> t array -> t array -> t 
+val mk_cofix_accu : int -> t array -> t array -> t
+val mk_meta_accu : metavariable -> t
+val mk_evar_accu : existential -> t -> t
 val upd_cofix : t -> t -> unit
 val force_cofix : t -> t 
 val mk_const : tag -> t
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index db858e0a0..f7805459f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -474,15 +474,16 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
     v2
 
 (* option for conversion *)
-let nat_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
+let nat_conv = ref (fun cv_pb sigma ->
+		    fconv cv_pb false (sigma.Nativelambda.evars_val))
 let set_nat_conv f = nat_conv := f
 
-let native_conv cv_pb env t1 t2 =
+let native_conv cv_pb sigma env t1 t2 =
   if eq_constr t1 t2 then empty_constraint
   else begin
     let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in
     let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in
-    !nat_conv cv_pb env t1 t2 
+    !nat_conv cv_pb sigma env t1 t2 
   end
 
 let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6e4634194..2d117cc96 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -55,8 +55,9 @@ val conv_leq_vecti :
 val set_vm_conv : (conv_pb -> types conversion_function) -> unit
 val vm_conv : conv_pb -> types conversion_function
 
-val set_nat_conv : (conv_pb -> types conversion_function) -> unit
-val native_conv : conv_pb -> types conversion_function
+val set_nat_conv :
+  (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit
+val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function
 
 val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
 val default_conv     : conv_pb -> ?l2r:bool -> types conversion_function
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a9cc151cf..6c4cb4574 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -271,8 +271,9 @@ let judge_of_cast env cj k tj =
           cj.uj_val,
           conv_leq true env cj.uj_type expected_type
       | NATIVEcast ->
-          mkCast (cj.uj_val, k, expected_type),
-          native_conv CUMUL env cj.uj_type expected_type
+	 let sigma = Nativelambda.empty_evars in
+         mkCast (cj.uj_val, k, expected_type),
+         native_conv CUMUL sigma env cj.uj_type expected_type
     in
     { uj_val = c;
       uj_type = expected_type },
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index ed52f574f..cc2054d10 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -21,9 +21,15 @@ open Nativecode
 open Inductiveops
 open Closure
 open Nativevalues
+open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
+let evars_of_evar_map evd =
+  { evars_val = Evd.existential_opt_value evd;
+    evars_typ = Evd.existential_type evd;
+    evars_metas = Evd.meta_type evd }
+
 exception Find_at of int
 
 let invert_tag cst tag reloc_tbl =
@@ -215,9 +221,14 @@ and nf_accu_type env accu =
 
 and nf_args env accu t =
   let aux arg (t,l) = 
-	let _,dom,codom = try decompose_prod env t with DestKO -> exit 123 in
-	let c = nf_val env arg dom in
-	(subst1 c codom, c::l)
+    let _,dom,codom =
+      try decompose_prod env t with
+	DestKO ->
+	Errors.anomaly
+	  (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+    in
+    let c = nf_val env arg dom in
+    (subst1 c codom, c::l)
   in
   let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in
   t, List.rev l
@@ -227,7 +238,12 @@ and nf_bargs env b t =
   let len = block_size b in
   Array.init len
     (fun i ->
-      let _,dom,codom = try decompose_prod env !t with DestKO -> exit 124 in
+      let _,dom,codom =
+	try decompose_prod env !t with
+	  DestKO ->
+	  Errors.anomaly
+	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+      in
       let c = nf_val env (block_field b i) dom in
       t := subst1 c codom; c)
 
@@ -244,9 +260,11 @@ and nf_atom env atom =
       let env = push_rel (n,None,dom) env in
       let codom = nf_type env (codom vn) in
       mkProd(n,dom,codom)
+  | Ameta (mv,_) -> mkMeta mv
+  | Aevar (ev,_) -> mkEvar ev
   | _ -> fst (nf_atom_type env atom)
 
-and nf_atom_type env atom = 
+and nf_atom_type env atom =
   match atom with
   | Arel i ->
       let n = (nb_rel env - i) in
@@ -308,13 +326,24 @@ and nf_atom_type env atom =
       let env = push_rel (n,None,dom) env in
       let codom,s2 = nf_type_sort env (codom vn) in
       mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
+  | Aevar(ev,ty) ->
+     let ty = nf_type env ty in
+     mkEvar ev, ty
+  | Ameta(mv,ty) ->
+     let ty = nf_type env ty in
+     mkMeta mv, ty
 
 and  nf_predicate env ind mip params v pT =
   match kind_of_value v, kind_of_term pT with
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = f (mk_rel_accu k) in
-      let name,dom,codom = try decompose_prod env pT with DestKO -> exit 121 in
+      let name,dom,codom =
+	try decompose_prod env pT with
+	  DestKO ->
+	  Errors.anomaly
+	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+      in
       let dep,body = 
 	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
       dep, mkLambda(name,dom,body)
@@ -330,7 +359,7 @@ and  nf_predicate env ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_type env v
 
-let native_norm env c ty =  
+let native_norm env sigma c ty =  
   if !Flags.no_native_compiler then
     error "Native_compute reduction has been disabled"
   else
@@ -340,7 +369,7 @@ let native_norm env c ty =
   Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
   *)
   let ml_filename, prefix = Nativelib.get_ml_filename () in
-  let code, upd = mk_norm_code penv prefix c in
+  let code, upd = mk_norm_code penv sigma prefix c in
   match Nativelib.compile ml_filename code with
     | 0,fn ->
         if !Flags.debug then Pp.msg_debug (Pp.str "Running norm ...");
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index ecc3489be..a589846b9 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -9,7 +9,11 @@ open Names
 open Term
 open Environ
 open Reduction
+open Evd
+open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-val native_norm : env -> constr -> types -> constr
+val evars_of_evar_map : evar_map -> evars
+
+val native_norm : env -> evars -> constr -> types -> constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a7e1cf481..74248301d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -709,17 +709,18 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 				   str "unresolved arguments remain.")
 	    | NATIVEcast ->
  	      let cj = pretype empty_tycon env evdref lvar c in
-	      let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
-		if not (occur_existential cty || occur_existential tval) then
-		  begin 
-		    try 
-		      ignore (Nativeconv.native_conv Reduction.CUMUL env cty tval); cj
-		    with Reduction.NotConvertible -> 
-		      error_actual_type_loc loc env !evdref cj tval 
-                        (ConversionFailed (env,cty,tval))
-		  end
-		else user_err_loc (loc,"",str "Cannot check cast with native compiler: " ++
-				   str "unresolved arguments remain.")
+	      let cty = nf_evar !evdref cj.uj_type and
+		  tval = nf_evar !evdref tj.utj_val in
+	      let evars = Nativenorm.evars_of_evar_map !evdref in
+	      begin
+	      try
+		ignore
+		  (Nativeconv.native_conv Reduction.CUMUL evars env cty tval);
+		cj
+	      with Reduction.NotConvertible -> 
+		error_actual_type_loc loc env !evdref cj tval 
+                  (ConversionFailed (env,cty,tval))
+	      end
 
 	    | _ -> 
  	      pretype (mk_tycon tval) env evdref lvar c
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index f71ec440e..db6f48547 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -29,9 +29,10 @@ let cbv_vm env sigma c =
     error "vm_compute does not support existential variables.";
   Vnorm.cbv_vm env c ctyp
 
-let cbv_native env _ c =
-  let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
-  Nativenorm.native_norm env c ctyp
+let cbv_native env sigma c =
+  let ctyp = Retyping.get_type_of env sigma c in
+  let evars = Nativenorm.evars_of_evar_map sigma in
+  Nativenorm.native_norm env evars c ctyp
 
 let set_strategy_one ref l  =
   let k =
@@ -212,7 +213,8 @@ let reduction_of_red_expr env =
     let lp = out_with_occurrences lp in
     let nativefun _ env map c =
       let tpe = Retyping.get_type_of env map c in
-      Nativenorm.native_norm env c tpe
+      let evars = Nativenorm.evars_of_evar_map map in
+      Nativenorm.native_norm env evars c tpe
     in
     let redfun = contextually b lp nativefun in
     (redfun, NATIVEcast)