blob: d82ddb416f42c0bc47d539165a2476fd3d9e4438 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
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].
|
