diff options
Diffstat (limited to 'plugins/fourier')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 6 | ||||
| -rw-r--r-- | plugins/fourier/fourier_plugin.mlpack (renamed from plugins/fourier/fourier_plugin.mllib) | 1 |
2 files changed, 3 insertions, 4 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index dc5dd45ab0..8e193c753e 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -462,7 +462,7 @@ let rec fourier () = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = strip_outer_cast concl in + let goal = Termops.strip_outer_cast 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 *) @@ -501,11 +501,11 @@ let rec fourier () = with NoIneq -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then Errors.error "No inequalities"; + if !lineq=[] then CErrors.error "No inequalities"; let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] - then Errors.error "fourier failed" + then CErrors.error "fourier failed" (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mlpack index 0383b1a80b..b6262f8aeb 100644 --- a/plugins/fourier/fourier_plugin.mllib +++ b/plugins/fourier/fourier_plugin.mlpack @@ -1,4 +1,3 @@ Fourier FourierR G_fourier -Fourier_plugin_mod |