Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v
new file mode 100644
index 00000000..802d8c97
--- /dev/null
+++ b/test-suite/output/SearchPattern.v
@@ -0,0 +1,19 @@
+(* Some tests of the SearchPattern command *)
+
+(* Simple, random tests *)
+SearchPattern bool.
+SearchPattern nat.
+SearchPattern le.
+
+(* With some hypothesis *)
+SearchPattern (nat -> nat).
+SearchPattern (?n * ?m + ?n = ?n * S ?m).
+
+(* Non-linearity *)
+SearchPattern (_ ?X ?X).
+
+(* Non-linearity with hypothesis *)
+SearchPattern (forall (x:?A) (y:?B), _ ?A ?B).
+
+(* No delta-reduction *)
+SearchPattern (Exc _).