From 3ef9c2e14138b3b6e41325d86844691e8579ee55 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 18 Dec 2012 00:46:03 +0000 Subject: No more constant named "int" in Coq theories (cf bug #2878) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16088 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/FMapAVL.v | 1 + 1 file changed, 1 insertion(+) (limited to 'theories/FSets') diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index a603751b2..f42f1e9e0 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -35,6 +35,7 @@ Module Raw (Import I:Int)(X: OrderedType). Local Open Scope pair_scope. Local Open Scope lazy_bool_scope. Local Open Scope Int_scope. +Local Notation int := I.t. Definition key := X.t. Hint Transparent key. -- cgit v1.2.3