From db37c9f3f32ae7a2abcd5e1a3f6239eddb5e1768 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 Jun 2014 13:01:31 +0200
Subject: Fix semantics of change p with c to typecheck c at each specific
 occurrence of p, avoiding unwanted universe constraints in presence of
 universe polymorphic constants. Fixing HoTT bugs # 36, 54 and 113.

---
 plugins/fourier/fourierR.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 1f6ece6025..7c134da7ac 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -587,7 +587,7 @@ let rec fourier gl=
                       else tac_zero_infeq_false gl (rational_to_fraction cres)
            in
            tac:=(tclTHENS (my_cut ineq)
-                     [tclTHEN (change_in_concl None
+                     [tclTHEN (change_concl
 			       (mkAppL [| get coq_not; ineq|]
 				       ))
 		      (tclTHEN (apply (if sres then get coq_Rnot_lt_lt
-- 
cgit v1.2.3