Merge PR #13597: Congruence: don't replace error messages by "congruence failed"

Reviewed-by: ejgallego
Ack-by: PierreCorbineau

4 files changed, 57 insertions, 47 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 23a7b89d2c..499c9684b2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -429,55 +429,55 @@ let cc_tactic depth additionnal_terms =
     match sol with
       None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
     | Some reason ->
-        debug (fun () -> Pp.str "Goal solved, generating proof ...");
-        match reason with
-          Discrimination (i,ipac,j,jpac) ->
-            let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
-            let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
-            discriminate_tac cstr p
-        | Incomplete ->
-      let open Glob_term in
-      let env = Proofview.Goal.env gl in
-      let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
-      let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
-      let pr_missing (c, missing) =
-        let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
-        let holes = List.init missing (fun _ -> hole) in
-        Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes))
-      in
-            let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
-                    ++ fnl () ++
-                    str "  Try " ++
-                    hov 8
-                    begin
-                      str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(")
-                      pr_missing terms_to_complete ++ str ")\","
-                    end ++
-                    str "  replacing metavariables by arbitrary terms.") in
-      Tacticals.New.tclFAIL 0 msg
-        | Contradiction dis ->
-      let env = Proofview.Goal.env gl in
-            let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
-            let ta=term uf dis.lhs and tb=term uf dis.rhs in
-            match dis.rule with
-              Goal -> proof_tac p
-            | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
-            | HeqG id ->
-                let id = EConstr.of_constr id in
-                convert_to_goal_tac id ta tb p
-            | HeqnH (ida,idb) ->
-                let ida = EConstr.of_constr ida in
-                let idb = EConstr.of_constr idb in
-                convert_to_hyp_tac ida ta idb tb p
+      debug (fun () -> Pp.str "Goal solved, generating proof ...");
+      match reason with
+        Discrimination (i,ipac,j,jpac) ->
+        let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
+        let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+        discriminate_tac cstr p
+      | Incomplete ->
+        let open Glob_term in
+        let env = Proofview.Goal.env gl in
+        let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+        let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
+        let pr_missing (c, missing) =
+          let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
+          let holes = List.init missing (fun _ -> hole) in
+          Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes))
+        in
+        let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
+                      ++ fnl () ++
+                      str "  Try " ++
+                      hov 8
+                        begin
+                          str "\"congruence with (" ++
+                          prlist_with_sep
+                            (fun () -> str ")" ++ spc () ++ str "(")
+                            pr_missing terms_to_complete ++
+                          str ")\","
+                        end ++
+                      fnl() ++ str "  replacing metavariables by arbitrary terms")
+        in
+        Tacticals.New.tclFAIL 0 msg
+      | Contradiction dis ->
+        let env = Proofview.Goal.env gl in
+        let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
+        let ta=term uf dis.lhs and tb=term uf dis.rhs in
+        match dis.rule with
+          Goal -> proof_tac p
+        | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
+        | HeqG id ->
+          let id = EConstr.of_constr id in
+          convert_to_goal_tac id ta tb p
+        | HeqnH (ida,idb) ->
+          let ida = EConstr.of_constr ida in
+          let idb = EConstr.of_constr idb in
+          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
diff --git a/test-suite/output/bug_13595.out b/test-suite/output/bug_13595.out
new file mode 100644
index 0000000000..2423b77b55
--- /dev/null
+++ b/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.
diff --git a/test-suite/output/bug_13595.v b/test-suite/output/bug_13595.v
new file mode 100644
index 0000000000..27a9ebe15d
--- /dev/null
+++ b/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.