aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/fourier/fourierR.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/fourier/fourierR.ml')
-rw-r--r--contrib/fourier/fourierR.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 03070ac92..3139db208 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -284,7 +284,7 @@ open Coqlib
let coq_sym_eqT = lazy (build_coq_sym_eqT ())
let coq_False = lazy (build_coq_False ())
let coq_not = lazy (build_coq_not ())
-let coq_eq = lazy (build_coq_eq_data.eq ())
+let coq_eq = lazy (build_coq_eq ())
(* Rdefinitions *)
let constant_real = constant ["Reals";"Rdefinitions"]