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
---
 test-suite/output/bug_13595.out | 4 ++++
 test-suite/output/bug_13595.v   | 8 ++++++++
 2 files changed, 12 insertions(+)
 create mode 100644 test-suite/output/bug_13595.out
 create mode 100644 test-suite/output/bug_13595.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3