diff options
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 429a0a4a8..f8b1927a3 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -463,7 +463,7 @@ let mkAppL a = let rec fourier gl= Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = strip_outer_cast (pf_concl gl) in - let fhyp=id_of_string "new_hyp_for_fourier" 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 *) try (let tac = |