aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/misc/coqc_dash_o.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-09 14:22:18 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-09 18:30:58 +0200
commit73e91542293af304ff25db9d3ea5495a9aa95249 (patch)
tree6cc38a97dc02eb30152c4d3ba4d6e6483a1fdfa6 /test-suite/misc/coqc_dash_o.v
parente9bd8cd805b7b350fe3a970e6be1c9ea2e88a1e8 (diff)
test for coqc -o
Diffstat (limited to 'test-suite/misc/coqc_dash_o.v')
-rw-r--r--test-suite/misc/coqc_dash_o.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/misc/coqc_dash_o.v b/test-suite/misc/coqc_dash_o.v
new file mode 100644
index 000000000..7426dff1a
--- /dev/null
+++ b/test-suite/misc/coqc_dash_o.v
@@ -0,0 +1 @@
+Definition x := nat.