aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/InitSyntax.v8
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/InitSyntax.v8')
-rw-r--r--test-suite/output/InitSyntax.v84
1 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/output/InitSyntax.v8 b/test-suite/output/InitSyntax.v8
deleted file mode 100644
index 66a01e145..000000000
--- a/test-suite/output/InitSyntax.v8
+++ /dev/null
@@ -1,4 +0,0 @@
-(* Soumis par Pierre *)
-Print sig2.
-Check (exists x : nat, x = x).
-Check (fun b : bool => if b then b else b). \ No newline at end of file