From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 theories/Init/Logic_Type.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'theories/Init/Logic_Type.v')

diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 2a833576..0281c516 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -44,7 +44,7 @@ Section identity_is_a_congruence.
 
  Lemma not_identity_sym : notT (identity x y) -> notT (identity y x).
  Proof.
-  red in |- *; intros H H'; apply H; destruct H'; trivial.
+  red; intros H H'; apply H; destruct H'; trivial.
  Qed.
 
 End identity_is_a_congruence.
@@ -66,7 +66,7 @@ Defined.
 
 Hint Immediate identity_sym not_identity_sym: core v62.
 
-Notation refl_id := identity_refl (only parsing).
-Notation sym_id := identity_sym (only parsing).
-Notation trans_id := identity_trans (only parsing).
-Notation sym_not_id := not_identity_sym (only parsing).
+Notation refl_id := identity_refl (compat "8.3").
+Notation sym_id := identity_sym (compat "8.3").
+Notation trans_id := identity_trans (compat "8.3").
+Notation sym_not_id := not_identity_sym (compat "8.3").
-- 
cgit v1.2.3