From b03ab4806e33a5f0a808d6325b87ab95189cd460 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 22 Apr 2004 10:21:05 +0000
Subject: Update to Coq 8.0 syntax

---
 coq/example.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'coq/example.v')

diff --git a/coq/example.v b/coq/example.v
index 6e88c5c8..95a9adac 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -5,9 +5,9 @@
 *)
 
 Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
-  intros A B H.
+  intros A B.
+  intros H.
   elim H.
-  intros.
   split.
   assumption.
   assumption.
-- 
cgit v1.2.3