diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 19:26:21 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
commit | a51dda2344679dc6d9145f3f34acad29721f6c75 (patch) | |
tree | c9ed50095ae459dabd97d9571566647439cf5269 /plugins/fourier/fourierR.ml | |
parent | b0ef649660542ae840ea945d7ab4f1f3ae7b85cd (diff) |
Split off Universes functions dealing with generating new universes.
Diffstat (limited to 'plugins/fourier/fourierR.ml')
-rw-r--r-- | plugins/fourier/fourierR.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 0ea70c19f..96be1d893 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -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"] |