diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-09-17 12:35:30 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-09-17 12:35:30 +0000 |
| commit | 85c4b9df59985030127cc8af25395db271952abf (patch) | |
| tree | a3680b7b246e02b258c5d0ef45a8f56f1bcc2c3b /etc | |
| parent | 56761b8fb30c6db4c9212fb779303fe5aaa5501e (diff) | |
New files.
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/coq/lostmessages.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/etc/coq/lostmessages.v b/etc/coq/lostmessages.v new file mode 100644 index 00000000..d82ddb41 --- /dev/null +++ b/etc/coq/lostmessages.v @@ -0,0 +1,13 @@ +(* These are some examples which generate goals and errors at the same + moment. May be broken in development version of Coq. + + See http://proofgeneral.inf.ed.ac.uk/trac/ticket/141 +*) + +Require Import Setoid. +Goal False. +setoid_replace False with True. + +Goal True /\ True -> True. +intro H. +destruct H as [H1 H2 H3]. |