2 files changed, 17 insertions, 19 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..e7c75e029e 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)
@@ -690,15 +690,13 @@ let ring_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    try (* find_ring_strucure can raise an exception *)
-      let rl = make_args_list sigma rl t in
-      let evdref = ref sigma in
-      let e = find_ring_structure env sigma rl in
-      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
-      let lH = carg (make_hyp_list env evdref lH) in
-      let ring = ltac_ring_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let rl = make_args_list sigma rl t in
+    let evdref = ref sigma in
+    let e = find_ring_structure env sigma rl in
+    let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
+    let lH = carg (make_hyp_list env evdref lH) in
+    let ring = ltac_ring_structure e in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
   end
 
 (***********************************************************************)
@@ -984,13 +982,11 @@ let field_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    try
-      let rl = make_args_list sigma rl t in
-      let evdref = ref sigma in
-      let e = find_field_structure env sigma rl in
-      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
-      let lH = carg (make_hyp_list env evdref lH) in
-      let field = ltac_field_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let rl = make_args_list sigma rl t in
+    let evdref = ref sigma in
+    let e = find_field_structure env sigma rl in
+    let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
+    let lH = carg (make_hyp_list env evdref lH) in
+    let field = ltac_field_structure e in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
   end