diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-01-25 15:24:21 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-25 15:24:21 +0000 |
| commit | 9442124c8204c6d8fec6fd1261fb2a19c9b6521b (patch) | |
| tree | 069918eda93668a88996c84ff10b6e36e694b4a6 /etc/coq | |
| parent | 2042769a3de38d3dff7b733f70fde783b2e3024e (diff) | |
Patch and cleanup for Coq indent code, see http://proofgeneral.inf.ed.ac.uk/trac/ticket/173
Diffstat (limited to 'etc/coq')
| -rw-r--r-- | etc/coq/indent.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/etc/coq/indent.v b/etc/coq/indent.v index 456018c6..46839715 100644 --- a/etc/coq/indent.v +++ b/etc/coq/indent.v @@ -58,5 +58,11 @@ Definition f := | # => # end end - +(* Nasty example from Trac http://proofgeneral.inf.ed.ac.uk/trac/ticket/173 *) +Theorem p : forall (P : Prop), P -> P. +Proof. + try (simpl + in *). + intros P H. apply H. +Qed. |