From 9edb5777f08f338367cd4384abdc17efcf2c2892 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 11:04:57 +0200
Subject: Simplify (restrict_path 0 sp) -> (make_path DirPath.empty id)

This is the only use of restrict_path so we just remove it.

The name collision between Libnames.make_path (takes a dirpath) and
Lib.make_path (uses current module+section path) is a bit awkward...
---
 library/libnames.ml  | 5 -----
 library/libnames.mli | 2 --
 tactics/declare.ml   | 4 ++--
 3 files changed, 2 insertions(+), 9 deletions(-)

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/tactics/declare.ml b/tactics/declare.ml
index e550e06471..dbf570eaad 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -301,7 +301,7 @@ type section_variable_entry =
 
 type variable_declaration = DirPath.t * section_variable_entry
 
-let cache_variable ((sp,_),o) =
+let cache_variable (_,o) =
   match o with
   | Inl ctx -> Global.push_context_set false ctx
   | Inr (id,(path,d),kind) ->
@@ -339,7 +339,7 @@ let cache_variable ((sp,_),o) =
       let () = Global.push_named_def (id, 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);
+  Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty id) (GlobRef.VarRef id);
   add_section_variable ~name:id ~kind:impl ~poly univs;
   Decls.(add_variable_data id {path;opaque;univs;poly;kind})
 
-- 
cgit v1.2.3


From 5a6de0ece2436a0fe49750ba0ec26da90f0417e3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 11:56:44 +0200
Subject: Remove constrintern global_level dead code

Not sure what this was for.
---
 interp/constrintern.ml  | 27 +++++++++++----------------
 interp/constrintern.mli |  4 ++--
 2 files changed, 13 insertions(+), 18 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index be8f99028c..eb4cd5b35e 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
@@ -2424,12 +2419,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 +2460,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))
 
-- 
cgit v1.2.3


From d324c858be652659a5062332f00e7d20393a48be Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 12:35:49 +0200
Subject: Safe_typing.push_named_assum: don't take universes

The caller should push them first
---
 kernel/safe_typing.ml  | 11 +++++------
 kernel/safe_typing.mli |  4 +---
 library/global.mli     |  2 +-
 tactics/declare.ml     |  5 +++--
 4 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2c434d4edf..084da42559 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -430,12 +430,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 885becc40a..721282ae50 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/tactics/declare.ml b/tactics/declare.ml
index dbf570eaad..ed745b1269 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -311,9 +311,10 @@ let cache_variable (_,o) =
 
   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 () = Global.push_context_set poly univs in
+      let () = Global.push_named_assum (id,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 *)
-- 
cgit v1.2.3


From bb81ed23c288f21f095d80a28ed7bda7ecf1a603 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 12:56:01 +0200
Subject: Search: do not use libobject to find variables

In preparation for removing the VARIABLE object.

It seems this doesn't change the output tests.
---
 vernac/search.ml | 51 ++++++++++++++++++++++++---------------------------
 1 file changed, 24 insertions(+), 27 deletions(-)

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 -> ()
-- 
cgit v1.2.3


From 4f0bdf2e19f0562a6cdf3b5ac075326b6e28c1d7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 13:02:57 +0200
Subject: Move declare_universe_context to top of Declare

In preparation for the other declarations to use it.
---
 tactics/declare.ml | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/tactics/declare.ml b/tactics/declare.ml
index ed745b1269..d93fcc0950 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 = {
@@ -553,19 +566,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
-- 
cgit v1.2.3


From 48a377680f4f3b96f7c19c22f5641877c561f03d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 13:51:49 +0200
Subject: Declare section variables in direct style "without" an object

The object was mostly for wrangling universes, but we already have the
universe object for that.

It's also used by some code which iterates over objects to find
variables.

Search used to do this but was changed in a previous commit.

Prettyp.print_context and derivatives do this and I don't understand
it enough to fix it, so I kept a dummy object around. It seems like a
not very common used Print family (not documented AFAICT) so maybe we
should remove it all instead.
---
 plugins/funind/indfun_common.ml |  2 +-
 tactics/declare.ml              | 59 +++++++++++++++--------------------------
 tactics/declare.mli             |  2 +-
 vernac/comAssumption.ml         |  2 +-
 vernac/declareDef.ml            |  5 ++--
 vernac/lemmas.ml                |  6 ++---
 6 files changed, 31 insertions(+), 45 deletions(-)

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 58b0ead130..ca19116ef0 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 (Lib.cwd(), 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 d93fcc0950..da3a119a79 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -314,18 +314,21 @@ type section_variable_entry =
 
 type variable_declaration = DirPath.t * section_variable_entry
 
-let cache_variable (_,o) =
-  match o with
-  | Inl ctx -> Global.push_context_set false ctx
-  | Inr (id,(path,d),kind) ->
+(* 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 declare_variable ~name ~kind (path,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_context_set poly univs in
-      let () = Global.push_named_assum (id,typ) 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
     | SectionLocalDef (de) ->
@@ -337,47 +340,29 @@ let cache_variable (_,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.make_path DirPath.empty id) (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 {path;opaque;univs;poly;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 =
diff --git a/tactics/declare.mli b/tactics/declare.mli
index f2d23fb319..3edb3f29cd 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -36,7 +36,7 @@ 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..520df1c21e 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -52,7 +52,7 @@ match scope with
   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 () = 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..2aa96fa8ed 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) (Lib.cwd(), 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..d6ee0b96f2 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 (Lib.cwd(),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 (Lib.cwd(), 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 (Lib.cwd(), c) in
           let () = if should_suggest
             then Proof_using.suggest_variable (Global.env ()) name
           in
-- 
cgit v1.2.3


From bffe3e43a51420293960cc3c32845687bdee5f9b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 13:59:17 +0200
Subject: Remove unused Decls.variable_{context,polymorphic}

---
 interp/decls.ml    | 4 ----
 interp/decls.mli   | 4 ----
 tactics/declare.ml | 2 +-
 3 files changed, 1 insertion(+), 9 deletions(-)

diff --git a/interp/decls.ml b/interp/decls.ml
index b802dbe9c3..ec5d4fa3cb 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -62,8 +62,6 @@ type logical_kind =
 type variable_data =
   { path:DirPath.t
   ; opaque:bool
-  ; univs:Univ.ContextSet.t
-  ; poly:bool
   ; kind:logical_kind
   }
 
@@ -75,8 +73,6 @@ let add_variable_data id o = vartab := Id.Map.add id o !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_secpath id =
   let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
diff --git a/interp/decls.mli b/interp/decls.mli
index 05e4be0de6..2a11a271cc 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -63,8 +63,6 @@ type logical_kind =
 type variable_data =
   { path:DirPath.t
   ; opaque:bool
-  ; univs:Univ.ContextSet.t
-  ; poly:bool
   ; kind:logical_kind
   }
 
@@ -81,6 +79,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/tactics/declare.ml b/tactics/declare.ml
index da3a119a79..91c55cacb0 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -359,7 +359,7 @@ let declare_variable ~name ~kind (path,d) =
   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 {path;opaque;univs;poly;kind});
+  Decls.(add_variable_data name {path;opaque;kind});
   add_anonymous_leaf (inVariable ());
   Impargs.declare_var_implicits name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
-- 
cgit v1.2.3


From 6e22817c6dab5043f1bdcbb1a1c8da281d4b3d7b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 3 Jul 2019 10:12:04 +0200
Subject: declare_variable: path is always Lib.cwd()

---
 interp/decls.ml                 | 19 +++++++++----------
 interp/decls.mli                |  9 ++++-----
 plugins/funind/indfun_common.ml |  2 +-
 tactics/declare.ml              |  8 +++-----
 tactics/declare.mli             |  4 +---
 vernac/comAssumption.ml         |  2 +-
 vernac/declareDef.ml            |  2 +-
 vernac/lemmas.ml                |  6 +++---
 8 files changed, 23 insertions(+), 29 deletions(-)

diff --git a/interp/decls.ml b/interp/decls.ml
index ec5d4fa3cb..ef22a393e4 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -59,20 +59,19 @@ type logical_kind =
 
 (** Data associated to section variables and local definitions *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque: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 add_variable_data id o = vartab := Id.Map.add id (o,Lib.cwd()) !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_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_secpath id =
   let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
diff --git a/interp/decls.mli b/interp/decls.mli
index 2a11a271cc..ba355999c2 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -60,11 +60,10 @@ type logical_kind =
 
 (** Registration and access to the table of variable *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque:bool
-  ; kind:logical_kind
-  }
+type variable_data = {
+  opaque:bool;
+  kind:logical_kind;
+}
 
 val add_variable_data : variable -> variable_data -> unit
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ca19116ef0..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 91c55cacb0..c0eae7503c 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -308,19 +308,17 @@ 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 declare_variable ~name ~kind (path,d) =
+let declare_variable ~name ~kind d =
   (* Constr raisonne sur les noms courts *)
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
@@ -359,7 +357,7 @@ let declare_variable ~name ~kind (path,d) =
   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 {path;opaque;kind});
+  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)
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 3edb3f29cd..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,8 +30,6 @@ 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
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 520df1c21e..c561d4a2a4 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -51,7 +51,7 @@ 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 decl = SectionLocalAssum {typ; univs; poly; impl} in
   let () = declare_variable ~name ~kind decl in
   let () = assumption_message name in
   let r = VarRef name in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 2aa96fa8ed..69338c0ba6 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -49,7 +49,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let gr = match scope with
   | Discharge ->
       let () =
-        declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce)
+        declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce)
       in
       VarRef name
   | Global local ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d6ee0b96f2..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
-- 
cgit v1.2.3


From d76a3591e091bb0807fa974c4098b32db9e6d1ad Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 3 Jul 2019 10:29:29 +0200
Subject: Remove unused variable_path (note secpath is still used)

---
 interp/decls.ml  | 6 +++---
 interp/decls.mli | 3 ---
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/interp/decls.ml b/interp/decls.ml
index ef22a393e4..d9d33b5e0b 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -67,14 +67,14 @@ type variable_data = {
 let vartab =
   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,Lib.cwd()) !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_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 ba355999c2..56866aeb43 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -67,9 +67,6 @@ type variable_data = {
 
 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
-- 
cgit v1.2.3


From 1cc661d18f67f71a494b525b1f82fd9133ee5a3c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 3 Jul 2019 10:40:38 +0200
Subject: Move variable_secpath logic to dumpglob from constrintern

---
 interp/constrintern.ml | 19 ++++++++++---------
 interp/dumpglob.ml     |  3 +++
 interp/dumpglob.mli    |  1 +
 3 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index eb4cd5b35e..68ade75815 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -949,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
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
-- 
cgit v1.2.3