Unset Asymmetric Patterns

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

5 files changed, 21 insertions, 21 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index f42f1e9e0..5d34a4bf5 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -342,7 +342,7 @@ Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
 
 Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
   match m with
-   | Leaf   => Leaf _
+   | Leaf _   => Leaf _
    | Node l x d r h => Node (map f l) x (f d) (map f r) h
   end.
 
@@ -350,7 +350,7 @@ Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
 
 Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
   match m with
-   | Leaf   => Leaf _
+   | Leaf _ => Leaf _
    | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h
   end.
 
@@ -359,7 +359,7 @@ Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
 Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
   : t elt' :=
   match m with
-   | Leaf => Leaf _
+   | Leaf _ => Leaf _
    | Node l x d r h =>
       match f x d with
        | Some d' => join (map_option f l) x d' (map_option f r)
@@ -389,8 +389,8 @@ Variable mapr : t elt' -> t elt''.
 
 Fixpoint map2_opt m1 m2 :=
  match m1, m2 with
-  | Leaf, _ => mapr m2
-  | _, Leaf => mapl m1
+  | Leaf _, _ => mapr m2
+  | _, Leaf _ => mapl m1
   | Node l1 x1 d1 r1 h1, _ =>
      let (l2',o2,r2') := split x1 m2 in
      match f x1 d1 o2 with
@@ -1424,7 +1424,7 @@ Qed.
     i.e. the list of elements actually compared *)
 
 Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
-  | End => nil
+  | End _ => nil
   | More x e t r => (x,e) :: elements t ++ flatten_e r
  end.
 
@@ -2016,7 +2016,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 :=
    match e2 with
-    | R.End => Gt
+    | R.End _ => Gt
     | R.More x2 d2 r2 e2 =>
        match X.compare x1 x2 with
         | EQ _ => match D.compare d1 d2 with
@@ -2033,7 +2033,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 :=
    match s1 with
-    | R.Leaf => cont e2
+    | R.Leaf _ => cont e2
     | R.Node l1 x1 d1 r1 _ =>
        compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2
    end.
@@ -2041,7 +2041,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   (** Initial continuation *)
 
   Definition compare_end (e2:R.enumeration D.t) :=
-   match e2 with R.End => Eq | _ => Lt end.
+   match e2 with R.End _ => Eq | _ => Lt end.
 
   (** The complete comparison *)
 
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index e1c603514..59b778369 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -660,7 +660,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Fixpoint cardinal_e (e:Raw.enumeration D.t) :=
     match e with
-     | Raw.End => 0%nat
+     | Raw.End _ => 0%nat
      | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e)
     end.
 
@@ -677,9 +677,9 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
    { measure cardinal_e_2 ee } : comparison :=
   match ee with
-  | (Raw.End, Raw.End) => Eq
-  | (Raw.End, Raw.More _ _ _ _) => Lt
-  | (Raw.More _ _ _ _, Raw.End) => Gt
+  | (Raw.End _, Raw.End _) => Eq
+  | (Raw.End _, Raw.More _ _ _ _) => Lt
+  | (Raw.More _ _ _ _, Raw.End _) => Gt
   | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
       match X.compare x1 x2 with
       | EQ _ => match D.compare d1 d2 with
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index d562245d8..5e968d4d3 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -902,7 +902,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
     Fixpoint xfoldi (m : t A) (v : B) (i : positive) :=
       match m with
-        | Leaf => v
+        | Leaf _ => v
         | Node l (Some x) r =>
           xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3)
         | Node l None r =>
@@ -940,8 +940,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool :=
     match m1, m2 with
-      | Leaf, _ => is_empty m2
-      | _, Leaf => is_empty m1
+      | Leaf _, _ => is_empty m2
+      | _, Leaf _ => is_empty m1
       | Node l1 o1 r1, Node l2 o2 r2 =>
            (match o1, o2 with
              | None, None => true
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 1ac544e1f..6aebcf501 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -284,7 +284,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
 
   Lemma choose_equal : forall s s', Equal s s' ->
      match choose s, choose s' with
-       | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+       | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
        | inright _, inright _  => True
        | _, _                        => False
      end.
@@ -423,7 +423,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition choose (s : t) : option elt :=
     match choose s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
@@ -472,7 +472,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition min_elt (s : t) : option elt :=
     match min_elt s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
@@ -500,7 +500,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition max_elt (s : t) : option elt :=
     match max_elt s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index a03611193..c791f49a6 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -497,7 +497,7 @@ Module Type Sdep.
         in the dependent version of [choose], so we leave it separate. *)
   Parameter choose_equal : forall s s', Equal s s' ->
      match choose s, choose s' with
-       | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+       | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
        | inright _, inright _  => True
        | _, _  => False
      end.