diff options
Diffstat (limited to 'plugins/fourier')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index d49f225e67..2a5e81ec0d 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -616,7 +616,7 @@ let rec fourier gl= ) ])); !tac1]); - tac:=(tclTHENS (cut (get coq_False)) + tac:=(tclTHENS (Proofview.V82.of_tactic (cut (get coq_False))) [tclTHEN (Proofview.V82.of_tactic intro) (Proofview.V82.of_tactic (contradiction None)); !tac]) |_-> assert false) |_-> assert false |