diff options
| author | Pierre-Marie Pédrot | 2018-10-19 15:27:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 15:27:55 +0200 |
| commit | 3799939088b5aa616974a0d37de7e2616024f222 (patch) | |
| tree | 808e60e5546489a694e1da784bd4895bc0195172 /plugins/nsatz | |
| parent | 6ab9a8088394b710ae0b9f6d5711d2fe0509419f (diff) | |
| parent | e050884da17b260934a428d5b1bb11cd788ae0e1 (diff) | |
Merge PR #8724: [universes] deprecate constr_of_global
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/nsatz.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 11d0a4a44d..ef60a23e80 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -135,7 +135,7 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let tpexpr = gen_constant "plugins.setoid_ring.pexpr" let ttconst = gen_constant "plugins.setoid_ring.const" @@ -540,7 +540,7 @@ let nsatz lpol = let return_term t = let a = - mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in + mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] |