diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-28 18:14:12 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-28 18:14:12 +0200 |
| commit | 132d40ae3168065ed9ca11aa12fc6c96111a1e67 (patch) | |
| tree | 3fe503493fce624caf8fd50d8580127bb8da0606 /plugins/nsatz/nsatz.ml | |
| parent | 422b892e71641f23dc71499733997546ecffa46b (diff) | |
| parent | 6841c6db48d57911d3886057e1ca47a5aa161ca7 (diff) | |
Merge PR#675: [coqlib] Deprecate redundant Coqlib functions.
Diffstat (limited to 'plugins/nsatz/nsatz.ml')
| -rw-r--r-- | plugins/nsatz/nsatz.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 632b9dac1..8c3471a98 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -134,8 +134,10 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let tpexpr = - lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") +let gen_constant msg path s = Universes.constr_of_global @@ + coq_reference msg path s + +let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc") let ttvar = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEX") let ttadd = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEadd") |