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.

1 files changed, 4 insertions, 3 deletions

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