aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/example.v
diff options
context:
space:
mode:
Diffstat (limited to 'coq/example.v')
-rw-r--r--coq/example.v5
1 files changed, 1 insertions, 4 deletions
diff --git a/coq/example.v b/coq/example.v
index f482f2ab..939f89c9 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -6,7 +6,7 @@
Module Example.
-Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
intros A B.
intros H.
elim H.
@@ -16,6 +16,3 @@ Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
Save and_comms.
End Example.
-
-
-