3 files changed, 8 insertions, 15 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 74043d6bc8..6f5c910297 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,19 +25,14 @@ open Util
 
 let init_size=5
 
-let cc_verbose=ref false
+let cc_verbose=
+  declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Congruence";"Verbose"]
+    ~value:false
 
 let debug x =
-  if !cc_verbose then Feedback.msg_debug (x ())
-
-let () =
-  let gdopt=
-    { optdepr=false;
-      optkey=["Congruence";"Verbose"];
-      optread=(fun ()-> !cc_verbose);
-      optwrite=(fun b -> cc_verbose := b)}
-  in
-    declare_bool_option gdopt
+  if cc_verbose () then Feedback.msg_debug (x ())
 
 (* Signature table *)
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0c305d09e8..c485c38009 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -290,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.enter begin fun gl ->
-  try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check (EConstr.of_constr c)
     | SymAx c ->
@@ -350,7 +349,6 @@ let rec proof_tac p : unit Proofview.tactic =
            app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
          Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
                                (Tacticals.New.tclTHEN injt (proof_tac prf))))
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let refute_tac c t1 t2 p =
@@ -508,11 +506,9 @@ let f_equal =
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let cut_eq c1 c2 =
-      try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
           (mk_eq _eq c1 c2 Tactics.cut)
           [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
-      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
       begin match EConstr.kind sigma concl with
diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/dune
index 2a92996d2a..f7fa3adb56 100644
--- a/plugins/cc/plugin_base.dune
+++ b/plugins/cc/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.cc)
  (synopsis "Coq's congruence closure plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_congruence))