coq.env.dependencies don't include the root

Author: gares

src/coq_elpi_builtins.ml

@@ -1121,6 +1121,7 @@ let dep1 ?inside sigma gr =
         if ModPath.equal (modpath_of_gref x) modpath
         then GRSet.add x acc
         else acc in
+<<<<<<< HEAD
   let add acc t = grefs_of_term sigma (EConstr.of_constr t) add_if_inside acc in
   match gr with
   | VarRef id ->
@@ -1145,6 +1146,41 @@ let dep1 ?inside sigma gr =
       let _, indbody = Global.lookup_inductive i in
       let l = indbody.Declarations.mind_user_lc in
       CArray.fold_left add GRSet.empty l
+=======
+  let rec add acc c =
+    let open Constr in
+    match kind c with
+      | Var x -> add_if_inside (VarRef x) acc
+      | Const (c,_) -> add_if_inside (ConstRef c) acc
+      | Ind (i,_) -> add_if_inside (IndRef i) acc
+      | Construct (k,_) -> add_if_inside (ConstructRef k) acc
+      | _ -> Constr.fold add acc c
+  in
+  GRSet.remove gr @@
+    match gr with
+    | VarRef id ->
+        let decl = Environ.lookup_named id (Global.env()) in
+        let ty = Context.Named.Declaration.get_type decl in
+        let bo = Context.Named.Declaration.get_value decl in
+        let l =
+          match bo with
+          | None -> [ty]
+          | Some bo -> [ty; bo] in
+        List.fold_left add GRSet.empty l
+    | ConstRef cst ->
+        let cb = Environ.lookup_constant cst (Global.env()) in
+        let ty = cb.Declarations.const_type in
+        let bo = Global.body_of_constant_body Library.indirect_accessor cb in
+        let l =
+          match bo with
+          | Some (e,_,_) -> [ty; e]
+          | None -> [ty] in
+        List.fold_left add GRSet.empty l
+    | IndRef i | ConstructRef (i,_) ->
+        let _, indbody = Global.lookup_inductive i in
+        let l = indbody.Declarations.mind_user_lc in
+        CArray.fold_left add GRSet.empty l
+>>>>>>> coq.env.dependencies don't include the root
 
 let universe_level_set, universe_level_set_decl =
   B.ocaml_set_conv ~name:"coq.univ.variable.set" universe_level_variable (module UnivLevelSet)
@@ -1688,7 +1724,7 @@ Supported attributes:
     In(B.unspec modpath, "MP",
     Out(gref_set, "Deps",
     Read(unit_ctx, "Computes the transitive dependencies of GR. If MP is given, Deps only contains grefs from that module")))),
-  (fun roots inside _ ~depth _ _ state ->
+  (fun root inside _ ~depth _ _ state ->
      let inside = unspec2opt inside in
      let sigma = get_sigma state in
      let rec aux seen = function
@@ -1703,6 +1739,7 @@ Supported attributes:
             let seen = GRSet.add x seen in
             aux seen (deps :: s :: rest)
      in
+<<<<<<< HEAD
      !: (aux GRSet.empty [dep1 ?inside sigma roots]))),
   DocAbove);
 
@@ -1714,6 +1751,9 @@ Supported attributes:
      let sigma = get_sigma state in
      let s = grefs_of_term sigma t GRSet.add GRSet.empty in
      state, !: s, [])),
+=======
+     !: (GRSet.remove root @@ aux GRSet.empty [dep1 ?inside root]))),
+>>>>>>> coq.env.dependencies don't include the root
   DocAbove);
 
   MLCode(Pred("coq.env.current-path",