Congruence: don't replace error messages by "congruence failed"

Fix #13595

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

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

test-suite/output/bug_13595.out

@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+Tactic failure: Goal is solvable by congruence but some arguments are missing.
+  Try "congruence with ((Triple a _ _)) ((Triple d c _))",
+  replacing metavariables by arbitrary terms.

test-suite/output/bug_13595.v

@@ -0,0 +1,8 @@
+Inductive Cube:Set :=| Triple: nat -> nat -> nat -> Cube.
+
+Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c.
+Proof.
+  Fail congruence.
+  intros.
+  congruence with ((Triple a a a)) ((Triple d c a)).
+Qed.