From 9f6e238fac96a123e7cb2bb2b2caec104bc4b916 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 18 Aug 2019 19:46:50 +0200
Subject: Declare universes for variables outside of Declare.declare_variable

(letins still declare universes in declare_variable as they use
entries)

The section check_same_poly is moved to declare_universe_context (it
makes more sense there, universe polymorphism doesn't apply to the
variables/letins themselves)
---
 tactics/declare.ml  | 12 +++++-------
 tactics/declare.mli |  2 +-
 2 files changed, 6 insertions(+), 8 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index e418240d3a..3ec6f884be 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -302,7 +302,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
+  | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; }
 
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
@@ -315,11 +315,10 @@ let declare_variable ~name ~kind d =
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
 
-  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 impl,opaque = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum {typ;impl} ->
       let () = Global.push_named_assum (name,typ) in
-      impl, true, poly
+      impl, true
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
@@ -342,8 +341,7 @@ let declare_variable ~name ~kind d =
         secdef_type = de.proof_entry_type;
       } in
       let () = Global.push_named_def (name, se) in
-      Glob_term.Explicit, de.proof_entry_opaque,
-      poly
+      Glob_term.Explicit, de.proof_entry_opaque
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
   Decls.(add_variable_data name {opaque;kind});
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 4cb876cecb..d479b75a28 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -36,7 +36,7 @@ type 'a proof_entry = {
 
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
+  | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
 
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
-- 
cgit v1.2.3