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