diff options
| author | Maxime Dénès | 2017-05-28 21:54:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-28 21:54:11 +0200 |
| commit | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (patch) | |
| tree | aea1f671a7486d7449ad6883f08e6e9a2ce4f744 /plugins/romega | |
| parent | fe62902764cc52daa985ad03e6f7ac0f8f1c2c4c (diff) | |
| parent | 5cc13770ac2358d583b21f217b8c65d2d5abd850 (diff) | |
Merge PR#678: [coqlib] Move `Coqlib` to `library/`.
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/const_omega.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index f38ca85b66..fbed1df176 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -63,13 +63,13 @@ let coq_modules = let bin_module = [["Coq";"Numbers";"BinNums"]] let z_module = [["Coq";"ZArith";"BinInt"]] -let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules -let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules -let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module -let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module +let init_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x +let constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" coq_modules x +let z_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" z_module x +let bin_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" bin_module x (* Logic *) -let coq_refl_equal = lazy(init_constant "eq_refl") +let coq_refl_equal = lazy(init_constant "eq_refl") let coq_and = lazy(init_constant "and") let coq_not = lazy(init_constant "not") let coq_or = lazy(init_constant "or") |