diff options
Diffstat (limited to 'etc/coq/lostmessages.v')
-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]. |