Fix handling of primitive projections in VM.

I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.

1 files changed, 18 insertions, 2 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b4492..83e566041 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -251,7 +251,24 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
 	match proj with
 	| None -> compile_constant_body env def
 	| Some pb ->
-	   compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
+	(* The compilation of primitive projections is a bit tricky, because
+           they refer to themselves (the body of p looks like fun c =>
+           Proj(p,c)). We break the cycle by building an ad-hoc compilation
+           environment. A cleaner solution would be that kernel projections are
+           simply Proj(i,c) with i an int and c a constr, but we would have to
+           get rid of the compatibility layer. *)
+	   let cb =
+	     { const_hyps = hyps;
+	       const_body = def;
+	       const_type = typ;
+	       const_proj = proj;
+	       const_body_code = None;
+	       const_polymorphic = poly;
+	       const_universes = univs;
+	       const_inline_code = inline_code }
+	   in
+	   let env = add_constant kn cb env in
+	   compile_constant_body env def
       in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
@@ -263,7 +280,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     const_universes = univs;
     const_inline_code = inline_code }
 
-
 (*s Global and local constant declaration. *)
 
 let translate_constant env kn ce =