diff options
Diffstat (limited to 'contrib/fourier')
| -rw-r--r-- | contrib/fourier/fourierR.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index c877dc47bb..2cdb929ae5 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -395,6 +395,7 @@ let mkAppL a = (* Résolution d'inéquations linéaires dans R *) let rec fourier gl= + Library.check_required_module ["Coq";"fourier";"Fourier"]; let parse = pf_parse_constr gl in let goal = strip_outer_cast (pf_concl gl) in let fhyp=id_of_string "new_hyp_for_fourier" in |