From f6a918174aa03408de960b85d4f95e33810949e8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Jan 2021 10:43:33 +0100
Subject: [PATCH] Test cases for `eunify`.

---
 tests/eunify.ref | 13 +++++++++++++
 tests/eunify.v   | 44 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 57 insertions(+)
 create mode 100644 tests/eunify.ref
 create mode 100644 tests/eunify.v

diff --git a/tests/eunify.ref b/tests/eunify.ref
new file mode 100644
index 00000000..2dc91ac7
--- /dev/null
+++ b/tests/eunify.ref
@@ -0,0 +1,13 @@
+"eunify_test"
+     : string
+The command has indeed failed with message:
+No matching clauses for match.
+((fix add (n m : nat) {struct n} : nat :=
+    match n with
+    | 0 => m
+    | S p => S (add p m)
+    end) x y)
+"eunify_test_evars"
+     : string
+The command has indeed failed with message:
+No matching clauses for match.
diff --git a/tests/eunify.v b/tests/eunify.v
new file mode 100644
index 00000000..c12cc618
--- /dev/null
+++ b/tests/eunify.v
@@ -0,0 +1,44 @@
+From stdpp Require Import tactics strings.
+
+Check "eunify_test".
+Lemma eunify_test : ∀ x y, 0 < S x + y.
+Proof.
+  intros x y.
+  (* Test that Ltac matching fails, otherwise this test is pointless *)
+  Fail
+    match goal with
+    | |- 0 < S _ => idtac
+    end.
+  (* [eunify] succeeds *)
+  match goal with
+  | |- 0 < ?x => eunify x (S _)
+  end.
+  match goal with
+  | |- 0 < ?x => let y := open_constr:(_) in eunify x (S y); idtac y
+  end.
+  lia.
+Qed.
+
+Check "eunify_test_evars".
+Lemma eunify_test_evars : ∃ x y, 0 < S x + y.
+Proof.
+  eexists _, _.
+  (* Test that Ltac matching fails, otherwise this test is pointless *)
+  Fail
+    match goal with
+    | |- 0 < S _ => idtac
+    end.
+  (* [eunify] succeeds even if the goal contains evars *)
+  match goal with
+  | |- 0 < ?x => eunify x (S _)
+  end.
+  (* Let's try to use [eunify] to instantiate the first evar *)
+  match goal with
+  | |- 0 < ?x => eunify x (1 + _)
+  end.
+  (* And the other evar *)
+  match goal with
+  | |- 0 < ?x => eunify x 2
+  end.
+  lia.
+Qed.
\ No newline at end of file
-- 
GitLab