{pattern} => in pattern;

[helm.git] / matita / matita / lib / arithmetics / chinese_reminder.ma

diff --git a/matita/matita/lib/arithmetics/chinese_reminder.ma b/matita/matita/lib/arithmetics/chinese_reminder.ma
index 77c0c7959e05150220e1cb657c86a5d68125c0e4..ec20f30dac3c73aa53bc0c8771cbd4239d85195b 100644 (file)
--- a/matita/matita/lib/arithmetics/chinese_reminder.ma
+++ b/matita/matita/lib/arithmetics/chinese_reminder.ma
@@ -118,7 +118,7 @@ theorem mod_cr_pair : ∀m,n,a,b. a < m → b < n → gcd n m = 1 →
 #m #n #a #b #ltam #ltbn #pnm 
 cut (andb (eqb ((cr_pair m n a b) \mod m) a) 
          (eqb ((cr_pair m n a b) \mod n) b) = true)
-  [whd {match (cr_pair m n a b)} @f_min_true cases(congruent_ab_lt m n a b ?? pnm)
+  [whd in match (cr_pair m n a b); @f_min_true cases(congruent_ab_lt m n a b ?? pnm)
     [#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/
      >eq_to_eqb_true
       [>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) //