diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-30 17:53:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:20:30 +0100 |
| commit | 5143129baac805d3a49ac3ee9f3344c7a447634f (patch) | |
| tree | 60fd3fb22fc95474454a6a60f3a8715bf7d766d0 /plugins/fourier/fourierR.ml | |
| parent | a42795cc1c2a8ed3efa9960af920ff7b16d928f0 (diff) | |
Termops API using EConstr.
Diffstat (limited to 'plugins/fourier/fourierR.ml')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 8e193c753..a14ec8a2c 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -461,8 +461,9 @@ exception GoalDone let rec fourier () = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = Termops.strip_outer_cast concl in + let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) |