From 47ea85e784d83aabddcc9250bfe565833d1e4462 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sun, 1 Jun 2008 22:56:50 +0000
Subject: Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in
 a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Cyclic/ZModulo/ZModulo.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/Cyclic/ZModulo')

diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index de7e4c6e89..b439462db3 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -806,7 +806,7 @@ Section ZModulo.
 
  clear; induction p.
  exists (Zpos p); simpl; rewrite Pmult_1_r; auto with zarith.
- destruct IHp as {y,Yp,Ye}.
+ destruct IHp as (y & Yp & Ye).
  exists y.
  split; auto.
  change (Zpos p~0) with (2*Zpos p).
-- 
cgit v1.2.3