From 2fa05a8d300f5c0d375a558a8bced972eea4bfaf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 7 Dec 2014 18:32:56 +0100
Subject: Moving change_in_concl, change_in_hyp, change_concl to
 Proofview.tactic.

---
 plugins/fourier/fourierR.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 551b210d37..4b70201b22 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -588,9 +588,9 @@ let rec fourier () =
                       else tac_zero_infeq_false gl (rational_to_fraction cres)
            in
            tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq))
-                     [Tacticals.New.tclTHEN (Proofview.V82.tactic (change_concl
+                     [Tacticals.New.tclTHEN (change_concl
 			       (mkAppL [| get coq_not; ineq|]
-				       )))
+				       ))
 		      (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
 					       else get coq_Rnot_le_le))
 			    (Tacticals.New.tclTHENS (Equality.replace
-- 
cgit v1.2.3