Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1515 r1521  
    3232   |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
    3333 #globals #def #left #right
    34  whd in match complete_regs normalize nodelta
     34 whd in match complete_regs; normalize nodelta
    3535 @leb_elim normalize nodelta #H
    36  [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
    37  | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
     36 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)));
     37 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)));]
    3838 cases (fresh_regs ????) #def' #fresh normalize >append_length
    39  generalize in match H -H;
    40  generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
    41  [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
     39 generalize in match H; -H;
     40 generalize in match (length … left); generalize in match (length … right); generalize in match (length … fresh);
     41 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H); -H #H #E >E >commutative_plus
    4242         <plus_minus_m_m /2/ ]
    4343qed.
Note: See TracChangeset for help on using the changeset viewer.