diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/dune (renamed from plugins/setoid_ring/plugin_base.dune) | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/dune index d83857edad..60522cd3f5 100644 --- a/plugins/setoid_ring/plugin_base.dune +++ b/plugins/setoid_ring/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.setoid_ring) (synopsis "Coq's setoid ring plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_newring)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0646af3552..633cdbd735 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -150,7 +150,7 @@ let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in - let () = Declare.declare_universe_context ~poly:false univs in + let () = DeclareUctx.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in mkConst(declare_constant ~name:(Id.of_string na) |