Remove the universe part from the section variable mechanism.

It was factorized away with the universe declaration entry. Actually,
pomlymorphic universes were declared twice in Declare, once as a context
extension, once as part of the variable itself.

3 files changed, 16 insertions, 17 deletions

diff --git a/library/lib.ml b/library/lib.ml
index cf7f97726a..fa383ab23c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -427,7 +427,6 @@ type secentry =
   | Variable of {
       id:Names.Id.t;
       kind:Decl_kinds.binding_kind;
-      univs:Univ.ContextSet.t;
     }
   | Context of Univ.ContextSet.t
 
@@ -454,12 +453,12 @@ let add_section ~poly () =
   List.iter (fun tab -> check_same_poly poly tab) !sectab;
   sectab := empty_section_data ~poly :: !sectab
 
-let add_section_variable ~name ~kind ~poly univs =
+let add_section_variable ~name ~kind ~poly =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | s :: sl ->
        List.iter (fun tab -> check_same_poly poly tab) !sectab;
-       let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in
+       let s = { s with sec_entry = Variable {id=name;kind} :: s.sec_entry } in
        sectab := s :: sl
 
 let add_section_context ctx =
@@ -470,31 +469,31 @@ let add_section_context ctx =
        let s = { s with sec_entry = Context ctx :: s.sec_entry } in
        sectab := s :: sl
 
-exception PolyFound of bool (* make this a let exception once possible *)
+exception PolyFound (* make this a let exception once possible *)
 let is_polymorphic_univ u =
   try
     let open Univ in
     List.iter (fun s ->
       let vars = s.sec_entry in
         List.iter (function
-            | Variable {univs=(univs,_)} ->
-              if LSet.mem u univs then raise (PolyFound s.sec_poly)
+            | Variable _ -> ()
             | Context (univs,_) ->
-              if LSet.mem u univs then raise (PolyFound true)
+              if LSet.mem u univs then raise PolyFound
           ) vars
       ) !sectab;
     false
-  with PolyFound b -> b
+  with PolyFound -> true
 
 let extract_hyps poly (secs,ohyps) =
   let rec aux = function
-    | (Variable {id;kind;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+    | (Variable {id;kind}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
       let l, r = aux (idl,hyps) in 
-      (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
-    | (Variable {univs}::idl,hyps) ->
+      (decl,kind) :: l, r
+    | (Variable _::idl,hyps) ->
         let l, r = aux (idl,hyps) in
-          l, if poly then Univ.ContextSet.union r univs else r
+          l, r
     | (Context ctx :: idl, hyps) ->
+      let () = assert poly in
        let l, r = aux (idl, hyps) in
        l, Univ.ContextSet.union r ctx
     | [], _ -> [],Univ.ContextSet.empty
diff --git a/library/lib.mli b/library/lib.mli
index b985c8c2bb..bfee1b16c5 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -183,7 +183,7 @@ val variable_section_segment_of_reference : GlobRef.t -> variable_context
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit
+val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> unit
 val add_section_context : Univ.ContextSet.t -> unit
 val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
 val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
diff --git a/tactics/declare.ml b/tactics/declare.ml
index b8ba62a5e5..63e9279edc 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -308,12 +308,12 @@ let declare_variable ~name ~kind d =
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
 
-  let impl,opaque,poly,univs = match d with (* Fails if not well-typed *)
+  let impl,opaque,poly = match d with (* Fails if not well-typed *)
     | SectionLocalAssum {typ;univs;poly;impl} ->
       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
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
@@ -338,10 +338,10 @@ let declare_variable ~name ~kind d =
       } in
       let () = Global.push_named_def (name, se) in
       Decl_kinds.Explicit, de.proof_entry_opaque,
-      poly, univs
+      poly
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
-  add_section_variable ~name ~kind:impl ~poly univs;
+  add_section_variable ~name ~kind:impl ~poly;
   Decls.(add_variable_data name {opaque;kind});
   add_anonymous_leaf (inVariable ());
   Impargs.declare_var_implicits name;