Unset Asymmetric Patterns

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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index e0bed0d37..9b8ebfe55 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -38,15 +38,15 @@ Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2.
 Proof.
 fix 3.
 refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh
-  with le_n => _ |le_S i H => _ end).
+  with le_n _ => _ |le_S _ i H => _ end).
 refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, 
   le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with
-    |le_n => fun eq => _ |le_S j H' => fun eq => _ end eq_refl).
+    |le_n _ => fun eq => _ |le_S _ j H' => fun eq => _ end eq_refl).
 rewrite (UIP_nat _ _ eq eq_refl). reflexivity.
 subst m. destruct (Lt.lt_irrefl j H').
 refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop
   with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h'
-    with |le_n => _ |le_S j H2 => fun H' => _ end H).
+    with |le_n _ => _ |le_S _ j H2 => fun H' => _ end H).
 destruct m. exact I. intros; destruct (Lt.lt_irrefl m H').
 f_equal. apply le_unique.
 Qed.