Unset Asymmetric Patterns

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

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d1610f0a1..6adc1c369 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -72,12 +72,12 @@ Section Subset_projections.
   Variable P : A -> Prop.
 
   Definition proj1_sig (e:sig P) := match e with
-                                    | exist a b => a
+                                    | exist _ a b => a
                                     end.
 
   Definition proj2_sig (e:sig P) :=
     match e return P (proj1_sig e) with
-    | exist a b => b
+    | exist _ a b => b
     end.
 
 End Subset_projections.
@@ -96,11 +96,11 @@ Section Projections.
   Variable P : A -> Type.
 
   Definition projT1 (x:sigT P) : A := match x with
-                                      | existT a _ => a
+                                      | existT _ a _ => a
                                       end.
   Definition projT2 (x:sigT P) : P (projT1 x) :=
     match x return P (projT1 x) with
-    | existT _ h => h
+    | existT _ _ h => h
     end.
 
 End Projections.