From 474a58b15ca41f1b3287ef3e29e80cca9988598c 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 | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index e50b0520bc..db7318469f 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -263,7 +263,10 @@ 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 (** This is a global universe context that shouldn't be
+	       refreshed at every use of the hint, declare it globally. *)
+	  (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


From 5b0b6c92354c34a4f0d5551f88b16264fb08be5f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 21 Oct 2016 10:49:15 +0200
Subject: Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3

This makes [refine] typecheck the term only once (instead of twice),
(Qed excluded of course). Fix test-suite file for output of constraints
accordingly.
---
 ltac/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index db7318469f..d0318fb5f6 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -355,7 +355,7 @@ let refine_tac ist simple c =
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
-    let refine = Refine.refine ~unsafe:false update in
+    let refine = Refine.refine ~unsafe:true update in
     if simple then refine
     else refine <*>
            Tactics.New.reduce_after_refine <*>
-- 
cgit v1.2.3