diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 01:25:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:43 +0100 |
| commit | 01849481fbabc3a3fa6c483e703996b01e37fca5 (patch) | |
| tree | 80798846a962da7754ddb0b3fae34434de3f7213 /plugins/fourier/fourierR.ml | |
| parent | 8beca748d992cd08e2dd7448c8b28dadbcea4a16 (diff) | |
Removing compatibility layers from Tacticals
Diffstat (limited to 'plugins/fourier/fourierR.ml')
| -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 bffca6223..ec73fccb5 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -616,7 +616,7 @@ let rec fourier () = (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) (Proofview.tclUNIT ()); Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq -> - (Tacticals.New.tclTHEN (apply (EConstr.of_constr symeq)) + (Tacticals.New.tclTHEN (apply symeq) (apply (get coq_Rinv_1))))] ) |