Merge branch 'v8.5' into trunk

1 files changed, 18 insertions, 2 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b4492b..83e566041f 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 =