From 83015147aac453effee4d5b1b6363b31c56edd84 Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 28 Sep 2007 22:36:35 +0000
Subject: Creation of a new token PATTERNIDENT (?ident) for intro patterns, so
 that "intros ? a ? b" behaves as expected.

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

(limited to 'theories/Ints')

diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v
index be7955aadd..cb6a01fcd3 100644
--- a/theories/Ints/Z/ZDivModAux.v
+++ b/theories/Ints/Z/ZDivModAux.v
@@ -142,7 +142,7 @@ Hint Resolve Zlt_gt Zle_ge: zarith.
   replace (c * a / b * b) with (c * a - (c * a) mod b).
   rewrite Zmult_minus_distr_l.
   unfold Zminus; apply Zplus_le_compat_l.
-  match goal with |- - ? X <= -?Y => assert (Y <= X); auto with zarith end.
+  match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end.
   apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
   rewrite Zmod_mult; case (Zmod_le_first ((c mod b) * (a mod b)) b); 
     auto with zarith.
-- 
cgit v1.2.3