From f4af5d4b09f262ef6388a2c0eeed85bf9b7ab3f9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 8 Dec 2020 10:33:42 +0100
Subject: Congruence: don't replace error messages by "congruence failed"

Fix #13595
---
 plugins/cc/cctac.ml  | 16 ++++++++--------
 plugins/cc/cctac.mli |  2 --
 2 files changed, 8 insertions(+), 10 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 12f80a17ed..499c9684b2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -450,10 +450,14 @@ let cc_tactic depth additionnal_terms =
                       str "  Try " ++
                       hov 8
                         begin
-                          str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(")
-                            pr_missing terms_to_complete ++ str ")\","
+                          str "\"congruence with (" ++
+                          prlist_with_sep
+                            (fun () -> str ")" ++ spc () ++ str "(")
+                            pr_missing terms_to_complete ++
+                          str ")\","
                         end ++
-                      str "  replacing metavariables by arbitrary terms.") in
+                      fnl() ++ str "  replacing metavariables by arbitrary terms")
+        in
         Tacticals.New.tclFAIL 0 msg
       | Contradiction dis ->
         let env = Proofview.Goal.env gl in
@@ -471,13 +475,9 @@ let cc_tactic depth additionnal_terms =
           convert_to_hyp_tac ida ta idb tb p
   end
 
-let cc_fail =
-  Tacticals.New.tclZEROMSG (Pp.str "congruence failed.")
 
 let congruence_tac depth l =
-  Tacticals.New.tclORELSE
-    (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l))
-    cc_fail
+  Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)
 
 (* Beware: reflexivity = constructor 1 = apply refl_equal
    might be slow now, let's rather do something equivalent
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 52fc3acb6f..79c7d2c676 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -14,8 +14,6 @@ val proof_tac: Ccproof.proof -> unit Proofview.tactic
 
 val cc_tactic : int -> constr list ->  unit Proofview.tactic
 
-val cc_fail : unit Proofview.tactic
-
 val congruence_tac : int -> constr list -> unit Proofview.tactic
 
 val f_equal : unit Proofview.tactic
-- 
cgit v1.2.3