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 b1c003de20..96be1d8934 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -227,7 +227,7 @@ let ineq1_of_constr (h,t) = hstrict=false}] |_-> raise NoIneq) | Ind ((kn,i),_) -> - if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; + if not (GlobRef.equal (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; let t0= args.(0) in let t1= args.(1) in let t2= args.(2) in @@ -283,15 +283,15 @@ let fourier_lineq lineq1 = let get = Lazy.force let cget = get let eget c = EConstr.of_constr (Lazy.force c) -let constant path s = Universes.constr_of_global @@ +let constant path s = UnivGen.constr_of_global @@ Coqlib.coq_reference "Fourier" path s (* Standard library *) open Coqlib let coq_sym_eqT = lazy (build_coq_eq_sym ()) -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 ()) +let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ()) +let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ()) +let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ()) (* Rdefinitions *) let constant_real = constant ["Reals";"Rdefinitions"] |