diff options
Diffstat (limited to 'plugins/fourier/fourierR.ml')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 484937858..1a629aac9 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -503,11 +503,11 @@ let rec fourier gl= with _ -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then Util.error "No inequalities"; + if !lineq=[] then Errors.error "No inequalities"; let res=fourier_lineq (!lineq) in let tac=ref tclIDTAC in if res=[] - then Util.error "fourier failed" + then Errors.error "fourier failed" (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> |