diff options
Diffstat (limited to 'plugins/fourier')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index d35e4ec6fa..a6290cb00c 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -291,9 +291,9 @@ let constant path s = Universes.constr_of_global @@ (* Standard library *) open Coqlib let coq_sym_eqT = lazy (build_coq_eq_sym ()) -let coq_False = lazy (build_coq_False ()) -let coq_not = lazy (build_coq_not ()) -let coq_eq = lazy (build_coq_eq ()) +let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ()) +let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ()) +let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ()) (* Rdefinitions *) let constant_real = constant ["Reals";"Rdefinitions"] @@ -514,11 +514,11 @@ let rec fourier () = with NoIneq -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then CErrors.error "No inequalities"; + if !lineq=[] then CErrors.user_err Pp.(str "No inequalities"); let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] - then CErrors.error "fourier failed" + then CErrors.user_err Pp.(str "fourier failed") (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> |