diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-09 14:22:18 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-09 18:30:58 +0200 |
commit | 73e91542293af304ff25db9d3ea5495a9aa95249 (patch) | |
tree | 6cc38a97dc02eb30152c4d3ba4d6e6483a1fdfa6 /test-suite/misc/coqc_dash_o.v | |
parent | e9bd8cd805b7b350fe3a970e6be1c9ea2e88a1e8 (diff) |
test for coqc -o
Diffstat (limited to 'test-suite/misc/coqc_dash_o.v')
-rw-r--r-- | test-suite/misc/coqc_dash_o.v | 1 |
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. |