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