From c7bd285555153294ec077cfa05c36bb420716f3b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 12 Apr 2018 21:41:03 +0200
Subject: Reduce circular dependency constants <-> projections

Instead of having the projection data in the constant data we have it
independently in the environment.
---
 kernel/nativecode.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 0cd0ad46c1..036cd4847e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1859,7 +1859,7 @@ and compile_named env sigma univ auxdefs id =
 
 let compile_constant env sigma prefix ~interactive con cb =
   match cb.const_proj with
-  | None ->
+  | false ->
      let no_univs =
        match cb.const_universes with
        | Monomorphic_const _ -> true
@@ -1903,7 +1903,8 @@ let compile_constant env sigma prefix ~interactive con cb =
 	  if interactive then LinkedInteractive prefix
 	  else Linked prefix
     end
-  | Some pb ->
+  | true ->
+      let pb = lookup_projection (Projection.make con false) env in
       let mind = pb.proj_ind in
       let ind = (mind,0) in
       let mib = lookup_mind mind env in
@@ -2029,11 +2030,12 @@ let rec compile_deps env sigma prefix ~interactive init t =
       else
       let comp_stack, (mind_updates, const_updates) =
 	match cb.const_proj, cb.const_body with
-        | None, Def t ->
+        | false, Def t ->
 	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
-	| Some pb, _ ->
-	   let mind = pb.proj_ind in
-	   compile_mind_deps env prefix ~interactive init mind
+        | true, _ ->
+          let pb = lookup_projection (Projection.make c false) env in
+          let mind = pb.proj_ind in
+          compile_mind_deps env prefix ~interactive init mind
         | _ -> init
       in
       let code, name =
-- 
cgit v1.2.3