aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/fourier
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-12-07 18:32:56 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-12-07 18:39:31 +0100
commit2fa05a8d300f5c0d375a558a8bced972eea4bfaf (patch)
treeecc7fa89b5f4be1bcc045fcd0d75e2b20f289566 /plugins/fourier
parent2acc6327e4d8a05898b75cb3abb47b7941ec420a (diff)
Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.
Diffstat (limited to 'plugins/fourier')
-rw-r--r--plugins/fourier/fourierR.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 551b210d3..4b70201b2 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