Merge PR #10461: Simplify Declare.declare_variable

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

18 files changed, 119 insertions, 162 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index be8f99028c..68ade75815 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -375,20 +375,17 @@ let check_hidden_implicit_parameters ?loc id impls =
 let pure_push_name_env (id,implargs) env =
   {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
 
-let push_name_env ?(global_level=false) ntnvars implargs env =
+let push_name_env ntnvars implargs env =
   let open CAst in
   function
   | { loc; v = Anonymous } ->
-      if global_level then
-	user_err ?loc (str "Anonymous variables not allowed");
       env
   | { loc; v = Name id } ->
       check_hidden_implicit_parameters ?loc id env.impls ;
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
         then error_ldots_var ?loc;
       set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
-      if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var"
-      else Dumpglob.dump_binding ?loc id;
+      Dumpglob.dump_binding ?loc id;
       pure_push_name_env (id,implargs) env
 
 let remember_binders_impargs env bl =
@@ -400,7 +397,7 @@ let remember_binders_impargs env bl =
 let restore_binders_impargs env l =
   List.fold_right pure_push_name_env l env
 
-let intern_generalized_binder ?(global_level=false) intern_type ntnvars
+let intern_generalized_binder intern_type ntnvars
     env {loc;v=na} b' t ty =
   let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
   let ty, ids' =
@@ -410,7 +407,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
   let ty' = intern_type {env with ids = ids; unb = true} ty in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
   let env' = List.fold_left
-    (fun env {loc;v=x} -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
+    (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
     env fvs in
   let bl = List.map
     CAst.(map (fun id ->
@@ -419,9 +416,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
   in
   let na = match na with
     | Anonymous ->
-	if global_level then na
-	else
-	  let name =
+          let name =
 	    let id =
 	      match ty with
               | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
@@ -430,7 +425,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
-  in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
+  in (push_name_env ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
 
 let intern_assumption intern ntnvars env nal bk ty =
   let intern_type env = intern (set_type_scope env) in
@@ -481,7 +476,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
   let na = make ?loc @@ Name id in
   env,((disjpat,il),id),na
 
-let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function
+let intern_local_binder_aux intern ntnvars (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern ntnvars env nal bk ty in
       let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
@@ -954,16 +949,17 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
     (* Is [id] a goal or section variable *)
     let _ = Environ.lookup_named_ctxt id namedctx in
       try
-	(* [id] a section variable *)
-	(* Redundant: could be done in intern_qualid *)
-	let ref = VarRef id in
-	let impls = implicits_of_global ref in
-	let scopes = find_arguments_scope ref in
-	Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	DAst.make ?loc @@ GRef (ref, us), impls, scopes, []
+        (* [id] a section variable *)
+        (* Redundant: could be done in intern_qualid *)
+        let ref = VarRef id in
+        let impls = implicits_of_global ref in
+        let scopes = find_arguments_scope ref in
+        Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *)
+        (* Someday we should stop relying on Dumglob raising exceptions *)
+        DAst.make ?loc @@ GRef (ref, us), impls, scopes, []
       with e when CErrors.noncritical e ->
-	(* [id] a goal variable *)
-	gvar (loc,id) us, [], [], []
+        (* [id] a goal variable *)
+        gvar (loc,id) us, [], [], []
 
 let find_appl_head_data c =
   match DAst.get c with
@@ -2424,12 +2420,12 @@ let interp_binder_evars env sigma na t =
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
 
-let intern_context global_level env impl_env binders =
+let intern_context env impl_env binders =
   try
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let lenv, bl = List.fold_left
 	    (fun (lenv, bl) b ->
-	       let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
+               let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
 	       (env, bl))
 	    ({ids = extract_ids env; unb = false;
 	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
@@ -2465,7 +2461,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
       (env,sigma,[],k+1,[]) (List.rev bl)
   in sigma, ((env, par), List.rev impls)
 
-let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
-  let int_env,bl = intern_context global_level env impl_env params in
+let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
+  let int_env,bl = intern_context env impl_env params in
   let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in
   sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 6c1f4898d9..2e7b832e55 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -90,7 +90,7 @@ val intern_gen : typing_constraint -> env -> evar_map ->
 val intern_pattern : env -> cases_pattern_expr ->
   lident list * (Id.t Id.Map.t * cases_pattern) list
 
-val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
+val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
@@ -158,7 +158,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map *
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
-  ?program_mode:bool -> ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
+  ?program_mode:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map -> local_binder_expr list ->
   evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))
 
diff --git a/interp/decls.ml b/interp/decls.ml
index b802dbe9c3..d9d33b5e0b 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -59,27 +59,22 @@ type logical_kind =
 
 (** Data associated to section variables and local definitions *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque:bool
-  ; univs:Univ.ContextSet.t
-  ; poly:bool
-  ; kind:logical_kind
-  }
+type variable_data = {
+  opaque:bool;
+  kind:logical_kind;
+}
 
 let vartab =
-  Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
+  Summary.ref (Id.Map.empty : (variable_data*DirPath.t) Id.Map.t) ~name:"VARIABLE"
 
-let add_variable_data id o = vartab := Id.Map.add id o !vartab
+let secpath () = drop_dirpath_prefix (Lib.library_dp()) (Lib.cwd())
+let add_variable_data id o = vartab := Id.Map.add id (o,secpath()) !vartab
 
-let variable_path id = let {path} = Id.Map.find id !vartab in path
-let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque
-let variable_kind id = let {kind} = Id.Map.find id !vartab in kind
-let variable_context id = let {univs} = Id.Map.find id !vartab in univs
-let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly
+let variable_opacity id = let {opaque},_ = Id.Map.find id !vartab in opaque
+let variable_kind id = let {kind},_ = Id.Map.find id !vartab in kind
 
 let variable_secpath id =
-  let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
+  let _, dir = Id.Map.find id !vartab in
   make_qualid dir id
 
 let variable_exists id = Id.Map.mem id !vartab
diff --git a/interp/decls.mli b/interp/decls.mli
index 05e4be0de6..56866aeb43 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -60,19 +60,13 @@ type logical_kind =
 
 (** Registration and access to the table of variable *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque:bool
-  ; univs:Univ.ContextSet.t
-  ; poly:bool
-  ; kind:logical_kind
-  }
+type variable_data = {
+  opaque:bool;
+  kind:logical_kind;
+}
 
 val add_variable_data : variable -> variable_data -> unit
 
-(* Not used *)
-val variable_path : variable -> DirPath.t
-
 (* Only used in dumpglob *)
 val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
@@ -81,6 +75,4 @@ val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
 
 (* Used in declare, very dubious *)
-val variable_context : variable -> Univ.ContextSet.t
-val variable_polymorphic : variable -> bool
 val variable_exists : variable -> bool
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 482303d935..dc6a1ae180 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -166,6 +166,9 @@ let dump_reference ?loc modpath ident ty =
   let filepath = Names.DirPath.to_string (Lib.library_dp ()) in
   dump_ref ?loc filepath modpath ident ty
 
+let dump_secvar ?loc id =
+  dump_reference ?loc "<>" (Libnames.string_of_qualid (Decls.variable_secpath id)) "var"
+
 let dump_modref ?loc mp ty =
   let (dp, l) = Lib.split_modpath mp in
   let filepath = Names.DirPath.to_string dp in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index e0308b8afc..60d62a1cb2 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -32,6 +32,7 @@ val dump_definition : Names.lident -> bool -> string -> unit
 val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_modref  : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_reference  : ?loc:Loc.t -> string -> string -> string -> unit
+val dump_secvar : ?loc:Loc.t -> Names.Id.t -> unit
 val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
   (Notation.notation_location * Notation_term.scope_name option) -> unit
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 445e359dee..24b3765019 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -428,12 +428,11 @@ let push_named_def (id,de) senv =
   let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in
   { senv with env = env'' }
 
-let push_named_assum ((id,t,poly),ctx) senv =
-  let senv' = push_context_set poly ctx senv in
-  let t, r = Term_typing.translate_local_assum senv'.env t in
-  let x = Context.make_annot id r in
-  let env'' = safe_push_named (LocalAssum (x,t)) senv'.env in
-    {senv' with env=env''}
+let push_named_assum (x,t) senv =
+  let t, r = Term_typing.translate_local_assum senv.env t in
+  let x = Context.make_annot x r in
+  let env'' = safe_push_named (LocalAssum (x,t)) senv.env in
+    {senv with env=env''}
 
 
 (** {6 Insertion of new declarations to current environment } *)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 50f6832ffa..c3d0965857 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -69,9 +69,7 @@ val is_joined_environment : safe_environment -> bool
 
 (** Insertion of local declarations (Local or Variables) *)
 
-val push_named_assum :
-  (Id.t * Constr.types * bool (* polymorphic *))
-    Univ.in_universe_context_set -> safe_transformer0
+val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
 
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
diff --git a/library/global.mli b/library/global.mli
index 51307b3604..d034bc4208 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -38,7 +38,7 @@ val sprop_allowed : unit -> bool
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_assum : (Id.t * Constr.types) -> unit
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 
 val export_private_constants : in_section:bool ->
diff --git a/library/libnames.ml b/library/libnames.ml
index 18af216e46..485f8837e8 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -128,11 +128,6 @@ let path_of_string s =
 
 let pr_path sp = str (string_of_path sp)
 
-let restrict_path n sp =
-  let dir, s = repr_path sp in
-  let dir' = List.firstn n (DirPath.repr dir) in
-  make_path (DirPath.make dir') s
-
 (*s qualified names *)
 type qualid_r = full_path
 type qualid = qualid_r CAst.t
diff --git a/library/libnames.mli b/library/libnames.mli
index 4455e29818..ffd7032fff 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -57,8 +57,6 @@ val pr_path : full_path -> Pp.t
 
 module Spmap  : CSig.MapS with type key = full_path
 
-val restrict_path : int -> full_path -> full_path
-
 (** {6 ... } *)
 (** A [qualid] is a partially qualified ident; it includes fully
     qualified names (= absolute names) and all intermediate partial
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 58b0ead130..c906670dc0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -128,7 +128,7 @@ let save name const ?hook uctx scope kind =
   let r = match scope with
     | Discharge ->
       let c = SectionLocalDef const in
-      let _ = declare_variable ~name ~kind (Lib.cwd(), c) in
+      let () = declare_variable ~name ~kind c in
       VarRef name
     | Global local ->
       let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index e550e06471..c0eae7503c 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -33,6 +33,19 @@ module NamedDecl = Context.Named.Declaration
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
+(** Monomorphic universes need to survive sections. *)
+
+let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
+  declare_object @@ local_object "Monomorphic section universes"
+    ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
+    ~discharge:(fun (_, x) -> Some x)
+
+let declare_universe_context ~poly ctx =
+  if poly then
+    (Global.push_context_set true ctx; Lib.add_section_context ctx)
+  else
+    Lib.add_anonymous_leaf (input_universe_context ctx)
+
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
@@ -295,25 +308,27 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   kn, eff
 
 (** Declaration of section variables and local definitions *)
-type section_variable_entry =
+type variable_declaration =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
-type variable_declaration = DirPath.t * section_variable_entry
+(* This object is only for things which iterate over objects to find
+   variables (only Prettyp.print_context AFAICT) *)
+let inVariable : unit -> obj =
+  declare_object { (default_object "VARIABLE") with
+    classify_function = (fun () -> Dispose)}
 
-let cache_variable ((sp,_),o) =
-  match o with
-  | Inl ctx -> Global.push_context_set false ctx
-  | Inr (id,(path,d),kind) ->
+let declare_variable ~name ~kind d =
   (* Constr raisonne sur les noms courts *)
-  if Decls.variable_exists id then
-    raise (AlreadyDeclared (None, id));
+  if Decls.variable_exists name then
+    raise (AlreadyDeclared (None, name));
 
   let impl,opaque,poly,univs = match d with (* Fails if not well-typed *)
     | SectionLocalAssum {typ;univs;poly;impl} ->
-      let () = Global.push_named_assum ((id,typ,poly),univs) in
+      let () = declare_universe_context ~poly univs in
+      let () = Global.push_named_assum (name,typ) in
       let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in
-        impl, true, poly, univs
+      impl, true, poly, univs
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
@@ -323,47 +338,29 @@ let cache_variable ((sp,_),o) =
       let eff = get_roles export eff in
       let () = List.iter register_side_effect eff in
       let poly, univs = match de.proof_entry_universes with
-      | Monomorphic_entry uctx -> false, uctx
-      | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+        | Monomorphic_entry uctx -> false, uctx
+        | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
       let univs = Univ.ContextSet.union uctx univs in
       (* We must declare the universe constraints before type-checking the
          term. *)
-      let () = Global.push_context_set (not poly) univs in
+      let () = declare_universe_context ~poly univs in
       let se = {
         secdef_body = body;
         secdef_secctx = de.proof_entry_secctx;
         secdef_feedback = de.proof_entry_feedback;
         secdef_type = de.proof_entry_type;
       } in
-      let () = Global.push_named_def (id, se) in
+      let () = Global.push_named_def (name, se) in
       Decl_kinds.Explicit, de.proof_entry_opaque,
-      poly, univs in
-  Nametab.push (Nametab.Until 1) (Libnames.restrict_path 0 sp) (GlobRef.VarRef id);
-  add_section_variable ~name:id ~kind:impl ~poly univs;
-  Decls.(add_variable_data id {path;opaque;univs;poly;kind})
-
-let discharge_variable (_,o) = match o with
-  | Inr (id,_,_) ->
-    if Decls.variable_polymorphic id then None
-    else Some (Inl (Decls.variable_context id))
-  | Inl _ -> Some o
-
-type variable_obj =
-    (Univ.ContextSet.t, Id.t * variable_declaration * Decls.logical_kind) union
-
-let inVariable : variable_obj -> obj =
-  declare_object { (default_object "VARIABLE") with
-    cache_function = cache_variable;
-    discharge_function = discharge_variable;
-    classify_function = (fun _ -> Dispose) }
-
-(* for initial declaration *)
-let declare_variable ~name ~kind obj =
-  let oname = add_leaf name (inVariable (Inr (name,obj,kind))) in
+      poly, univs
+  in
+  Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
+  add_section_variable ~name ~kind:impl ~poly univs;
+  Decls.(add_variable_data name {opaque;kind});
+  add_anonymous_leaf (inVariable ());
   Impargs.declare_var_implicits name;
-  Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name);
-  oname
+  Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
 (** Declaration of inductive blocks *)
 let declare_inductive_argument_scopes kn mie =
@@ -552,19 +549,6 @@ let assumption_message id =
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
   Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
 
-(** Monomorphic universes need to survive sections. *)
-
-let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
-  declare_object @@ local_object "Monomorphic section universes"
-    ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
-    ~discharge:(fun (_, x) -> Some x)
-
-let declare_universe_context ~poly ctx =
-  if poly then
-    (Global.push_context_set true ctx; Lib.add_section_context ctx)
-  else
-    Lib.add_anonymous_leaf (input_universe_context ctx)
-
 (** Global universes are not substitutive objects but global objects
    bound at the *library* or *module* level. The polymorphic flag is
    used to distinguish universes declared in polymorphic sections, which
diff --git a/tactics/declare.mli b/tactics/declare.mli
index f2d23fb319..89b41076f7 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -21,7 +21,7 @@ open Entries
 
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
-type section_variable_entry =
+type variable_declaration =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
@@ -30,13 +30,11 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-type variable_declaration = DirPath.t * section_variable_entry
-
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
   -> variable_declaration
-  -> Libobject.object_name
+  -> unit
 
 (** Declaration of global constructions
    i.e. Definition/Theorem/Axiom/Parameter/... *)
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 -> ()