From 7ada864b7728c9c94b7ca9856b6b2c89feb0214e Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Wed, 30 May 2018 18:20:52 +0200
Subject: Fix #7631: native_compute fails to compile an example in Coq 8.8

Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
---
 kernel/nativecode.ml | 43 +++++++++++++++++++++++++++++++------------
 1 file changed, 31 insertions(+), 12 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 036cd4847..5174eeea8 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2017,21 +2017,22 @@ 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 sigma prefix ~interactive init t =
+let compile_deps env sigma prefix ~interactive init t =
+  let rec aux env lvl init t =
   match kind t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
-      let c,u = get_alias env c in
-      let cb,(nameref,_) = lookup_constant_key c env in
-      let (_, (_, const_updates)) = init in
-      if is_code_loaded ~interactive nameref
-        || (Cmap_env.mem c const_updates)
-      then init
-      else
+    let c,u = get_alias env c in
+    let cb,(nameref,_) = lookup_constant_key c env in
+    let (_, (_, const_updates)) = init in
+    if is_code_loaded ~interactive nameref
+    || (Cmap_env.mem c const_updates)
+    then init
+    else
       let comp_stack, (mind_updates, const_updates) =
 	match cb.const_proj, cb.const_body with
         | false, Def t ->
-	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+           aux env lvl init (Mod_subst.force_constr t)
         | true, _ ->
           let pb = lookup_projection (Projection.make c false) env in
           let mind = pb.proj_ind in
@@ -2047,12 +2048,30 @@ let rec compile_deps env sigma prefix ~interactive init t =
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
     let term = mkApp (mkConst (Projection.constant p), [|c|]) in
-      compile_deps env sigma prefix ~interactive init term
+    aux env lvl init term
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
-      Constr.fold (compile_deps env sigma prefix ~interactive) init t
-  | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t
+      fold_constr_with_binders succ (aux env) lvl init t
+  | Var id ->
+    let open Context.Named.Declaration in
+    begin match lookup_named id env with
+      | LocalDef (_,t,_) ->
+        aux env lvl init t
+      | _ -> init
+    end
+  | Rel n when n > lvl ->
+    let open Context.Rel.Declaration in
+    let decl = lookup_rel n env in
+    let env = env_of_rel n env in
+    begin match decl with
+    | LocalDef (_,t,_) ->
+      aux env lvl init t
+    | LocalAssum _ -> init
+    end
+  | _ -> fold_constr_with_binders succ (aux env) lvl init t
+  in
+  aux env 0 init t
 
 let compile_constant_field env prefix con acc cb =
     let (gl, _) =
-- 
cgit v1.2.3