Test cases for `eunify`.

tests/eunify.ref

+"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.

tests/eunify.v

+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