From cf87e73ff4dd0b9c70436d66d326ae839868ba78 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Sep 2016 17:26:14 +0200
Subject: Fix bug #5036 autorewrite, sections and universes

Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
---
 ltac/extratactics.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'ltac')

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
-- 
cgit v1.2.3