diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-17 10:31:55 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-17 10:31:55 +0000 |
| commit | 4e41135d9aa09260ccf1ca801ac055fd71838a7e (patch) | |
| tree | dc8f53892869c633b9fc21b7d36c911e6cc74d65 /test-suite/success/bullet.v | |
| parent | 5b9981239c3192d20d7db2de1248a63b59cbf44a (diff) | |
Add simple test of bullet behaviour.
Signed-off-by: Tom Prince <tom.prince@ualberta.net>
Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14132 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/bullet.v')
| -rw-r--r-- | test-suite/success/bullet.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/bullet.v b/test-suite/success/bullet.v new file mode 100644 index 000000000..1099f3e19 --- /dev/null +++ b/test-suite/success/bullet.v @@ -0,0 +1,5 @@ +Goal True /\ True. +split. +- exact I. +- exact I. +Qed. |