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.

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