Changeset 1521 for src/RTLabs

Timestamp:

Nov 21, 2011, 1:06:01 PM (8 years ago)

Author:

sacerdot

Message:

Syntax change in Matita: change what where => change where what.

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (1 diff)

src/RTLabs/RTLabsToRTL.ma

@@ -32 +32 @@
    |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
  #globals #def #left #right
- whd in match complete_regs normalize nodelta
+ whd in match complete_regs; normalize nodelta
  @leb_elim normalize nodelta #H
- [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
- | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
+ [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)));
+ | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)));]
  cases (fresh_regs ????) #def' #fresh normalize >append_length
- generalize in match H -H;
- generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
- [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
+ generalize in match H; -H;
+ generalize in match (length … left); generalize in match (length … right); generalize in match (length … fresh);
+ [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H); -H #H #E >E >commutative_plus
          <plus_minus_m_m /2/ ]
 qed.