From 99dfd9ba50a40df6c3d558b84ce2a8284ab16fa0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 20 May 2006 00:41:35 +0000
Subject: suite tentative pour permettre l'utilisation de modules de FSets avec
 <: au lieu de : sans surprise de modules genre Raw partout ou autres alias
 dépliés

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8834 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/OrderedType.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'theories/FSets/OrderedType.v')

diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index 0268b38c9f..d989d8937d 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -313,6 +313,8 @@ Ltac false_order := elimtype False; order.
 
 (* Specialization of resuts about lists modulo. *)
 
+Section ForNotations.
+
 Notation In:=(InA eq).
 Notation Inf:=(lelistA lt).
 Notation Sort:=(sort lt).
@@ -346,6 +348,8 @@ Proof. exact (InfA_alt eq_refl eq_sym lt_trans lt_eq eq_lt). Qed.
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
 Proof. exact (SortA_NoDupA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed.
 
+End ForNotations.
+
 Hint Resolve ListIn_In Sort_NoDup Inf_lt. 
 Hint Immediate In_eq Inf_lt. 
 
-- 
cgit v1.2.3