Merge branch 'bug5036' into v8.6

4 files changed, 36 insertions, 7 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 3d063225f4..7d32b93dc5 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -434,6 +434,23 @@ let assumption_message id =
 
 (** Global universe names, in a different summary *)
 
+type universe_context_decl = polymorphic * Univ.universe_context_set
+
+let cache_universe_context (p, ctx) =
+  Global.push_context_set p ctx;
+  if p then Lib.add_section_context ctx
+
+let input_universe_context : universe_context_decl -> Libobject.obj =
+  declare_object
+    { (default_object "Global universe context state") with
+      cache_function = (fun (na, pi) -> cache_universe_context pi);
+      load_function = (fun _ (_, pi) -> cache_universe_context pi);
+      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+      classify_function = (fun a -> Keep a) }
+
+let declare_universe_context poly ctx =
+  Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
+
 (* Discharged or not *)
 type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
 
@@ -446,9 +463,8 @@ let cache_universes (p, l) =
          Univ.ContextSet.add_universe lev ctx))
       (glob, Univ.ContextSet.empty) l
   in
-    Global.push_context_set p ctx;
-    if p then Lib.add_section_context ctx;
-    Universes.set_global_universe_names glob'
+  cache_universe_context (p, ctx);
+  Universes.set_global_universe_names glob'
 
 let input_universes : universe_decl -> Libobject.obj =
   declare_object
@@ -475,8 +491,8 @@ let do_universe poly l =
 type constraint_decl = polymorphic * Univ.constraints
 
 let cache_constraints (na, (p, c)) =
-  Global.add_constraints c;
-  if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)
+  let ctx = Univ.ContextSet.add_constraints c Univ.ContextSet.empty in
+  cache_universe_context (p,ctx)
 
 let discharge_constraints (_, (p, c as a)) =
   if p then None else Some a
diff --git a/library/declare.mli b/library/declare.mli
index 7824506da0..e614f5206a 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -87,7 +87,9 @@ val exists_name : Id.t -> bool
 
 
 
-(** Global universe names and constraints *)
+(** Global universe contexts, names and constraints *)
+
+val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit
 
 val do_universe : polymorphic -> Id.t Loc.located list -> unit
 val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index e50b0520bc..d6ba670d83 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -263,7 +263,8 @@ let add_rewrite_hint bases ort t lcsr =
     let ctx =
       let ctx = UState.context_set ctx in
         if poly then ctx
-	else (Global.push_context_set false ctx; Univ.ContextSet.empty)
+	else (Declare.declare_universe_context false ctx;
+              Univ.ContextSet.empty)
     in
       Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in
   let eqs = List.map f lcsr in
diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v
new file mode 100644
index 0000000000..12c958be67
--- /dev/null
+++ b/test-suite/bugs/closed/5036.v
@@ -0,0 +1,10 @@
+Section foo.
+  Context (F : Type -> Type).
+  Context (admit : forall {T}, F T = True).
+  Hint Rewrite (fun T => @admit T).
+  Lemma bad : F False.
+  Proof.
+    autorewrite with core.
+    constructor.
+  Qed.
+End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file