Merge PR #10461: Simplify Declare.declare_variable

Reviewed-by: ejgallego
Reviewed-by: maximedenes
Reviewed-by: ppedrot

4 files changed, 32 insertions, 34 deletions

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 60086a7861..c561d4a2a4 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -51,8 +51,8 @@ match scope with
     | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
   in
   let kind = Decls.IsAssumption kind in
-  let decl = Lib.cwd(), SectionLocalAssum {typ; univs; poly; impl} in
-  let _ = declare_variable ~name ~kind decl in
+  let decl = SectionLocalAssum {typ; univs; poly; impl} in
+  let () = declare_variable ~name ~kind decl in
   let () = assumption_message name in
   let r = VarRef name in
   let () = maybe_declare_manual_implicits true r imps in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 4dcb3db63b..69338c0ba6 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -48,8 +48,9 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
   let gr = match scope with
   | Discharge ->
-      let _ : Libobject.object_name =
-        declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce) in
+      let () =
+        declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce)
+      in
       VarRef name
   | Global local ->
       let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d0e2e0f935..ea735dd7f9 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -266,7 +266,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
           | Monomorphic_entry univs -> univs
         in
         let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in
-        let _ = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in
+        let () = Declare.declare_variable ~name ~kind c in
         (VarRef name,impargs)
       | Global local ->
         let kind = Decls.(IsAssumption Conjectural) in
@@ -289,7 +289,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
       | Discharge ->
         let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
         let c = Declare.SectionLocalDef const in
-        let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
+        let () = Declare.declare_variable ~name ~kind c in
         (VarRef name,impargs)
       | Global local ->
         let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in
@@ -499,7 +499,7 @@ let finish_proved env sigma idopt po info =
       let r = match scope with
         | Discharge ->
           let c = Declare.SectionLocalDef const in
-          let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
+          let () = Declare.declare_variable ~name ~kind c in
           let () = if should_suggest
             then Proof_using.suggest_variable (Global.env ()) name
           in
diff --git a/vernac/search.ml b/vernac/search.ml
index 4af14e895d..101a578587 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -75,35 +75,32 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
 (* General search over declarations *)
 let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
   let env = Global.env () in
+  List.iter (fun d -> fn (VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d))
+    (Environ.named_context env);
   let iter_obj (sp, kn) lobj = match lobj with
-  | AtomicObject o ->
-    begin match object_tag o with
-    | "VARIABLE" ->
-      begin try
-        let decl = Global.lookup_named (basename sp) in
-        fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl)
-      with Not_found -> (* we are in a section *) () end
-    | "CONSTANT" ->
-      let cst = Global.constant_of_delta_kn kn in
-      let gr = ConstRef cst in
-      let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
-      fn gr env typ
-    | "INDUCTIVE" ->
-      let mind = Global.mind_of_delta_kn kn in
-      let mib = Global.lookup_mind mind in
-      let iter_packet i mip =
-        let ind = (mind, i) in
-        let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
-        let i = (ind, u) in
-        let typ = Inductiveops.type_of_inductive env i in
-        let () = fn (IndRef ind) env typ in
-        let len = Array.length mip.mind_user_lc in
-        iter_constructors ind u fn env len
-      in
-      Array.iteri iter_packet mib.mind_packets
+    | AtomicObject o ->
+      begin match object_tag o with
+        | "CONSTANT" ->
+          let cst = Global.constant_of_delta_kn kn in
+          let gr = ConstRef cst in
+          let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
+          fn gr env typ
+        | "INDUCTIVE" ->
+          let mind = Global.mind_of_delta_kn kn in
+          let mib = Global.lookup_mind mind in
+          let iter_packet i mip =
+            let ind = (mind, i) in
+            let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+            let i = (ind, u) in
+            let typ = Inductiveops.type_of_inductive env i in
+            let () = fn (IndRef ind) env typ in
+            let len = Array.length mip.mind_user_lc in
+            iter_constructors ind u fn env len
+          in
+          Array.iteri iter_packet mib.mind_packets
+        | _ -> ()
+      end
     | _ -> ()
-    end
-  | _ -> ()
   in
   try Declaremods.iter_all_segments iter_obj
   with Not_found -> ()