From 6841c6db48d57911d3886057e1ca47a5aa161ca7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 23 Feb 2016 01:35:00 +0100 Subject: [coqlib] Deprecate redundant Coqlib functions. We remove redundant functions `coq_constant`, `gen_reference`, and `gen_constant`. This is a first step towards a lazy binding of libraries references. We have also chosen to untangle `constr` from `Coqlib`, as how to instantiate the reference (in particular wrt universes) is a client-side issue. (The client may want to provide an `evar_map` ?) c.f. #186 --- plugins/nsatz/nsatz.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'plugins/nsatz') 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") -- cgit v1.2.3