diff options
Diffstat (limited to 'contrib/fourier/fourierR.ml')
| -rw-r--r-- | contrib/fourier/fourierR.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 33d6faad1..5e31d5675 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -458,7 +458,7 @@ let mkAppL a = (* Résolution d'inéquations linéaires dans R *) let rec fourier gl= - Library.check_required_library ["Coq";"fourier";"Fourier"]; + 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 (* si le but est une inéquation, on introduit son contraire, |