Make PositiveMap.xmapi structural

With the previous definition, it was e.g. impossible to define a
fixpoint for the inductive type:
  Inductive t : Set := T : PositiveMap.t t -> t.
using PositiveMap.map.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11664 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 9 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 6903b67ae..a0849f675 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -820,16 +820,21 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
  
   Variable B : Type.
 
-  Fixpoint xmapi (f : positive -> A -> B) (m : t A) (i : positive)
-             {struct m} : t B :=
-     match m with
-      | Leaf => @Leaf B
-      | Node l o r => Node (xmapi f l (append i (xO xH)))
-                           (option_map (f i) o)
-                           (xmapi f r (append i (xI xH)))
-     end.
+  Section Mapi.
+
+    Variable f : positive -> A -> B.
+
+    Fixpoint xmapi (m : t A) (i : positive) {struct m} : t B :=
+       match m with
+        | Leaf => @Leaf B
+        | Node l o r => Node (xmapi l (append i (xO xH)))
+                             (option_map (f i) o)
+                             (xmapi r (append i (xI xH)))
+       end.
+
+    Definition mapi m := xmapi m xH.
 
-  Definition mapi (f : positive -> A -> B) m := xmapi f m xH.
+  End Mapi.
 
   Definition map (f : A -> B) m := mapi (fun _ => f) m.