Changeset 1521 for src/Cminor


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/Cminor/toRTLabs.ma

    r1516 r1521  
    2828      whd in E:(??%?); destruct;
    2929      whd >lookup_add_hit % #A destruct
    30     | #H change in E:(??(match % with [ _ ⇒ ? ])?); with (populate_env e u tl)
     30    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
    3131      lapply (refl ? (populate_env e u tl))
    3232      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
     
    4444[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
    4545| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
    46   change in E:(??(match % with [ _ ⇒ ?])?); with (populate_env e u tl)
     46  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
    4747  lapply (refl ? (populate_env e u tl))
    4848  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
     
    6565[ #lbls #u #lbls' #u' #E #l *
    6666| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
    67   change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
     67  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
    6868  lapply (refl ? (populate_label_env lbls u t))
    6969  cases (populate_label_env lbls u t) in ⊢ (???% → %);
     
    8282[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
    8383| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
    84   change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
     84  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
    8585  lapply (refl ? (populate_label_env lbls u t))
    8686  cases (populate_label_env lbls u t) in ⊢ (???% → %);
Note: See TracChangeset for help on using the changeset viewer.