Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r1515 r1516  
    2121 #pars0 #globals #def #n elim n
    2222  [ %
    23   | #m whd in ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?)
     23  | #m whd in ⊢ (? → ??(??%)?); whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) ;
    2424    cases (fresh_regs pars0 globals def m) normalize nodelta
    25     #def' #regs #EQ change in EQ with (|regs| = m) <EQ
     25    #def' #regs #EQ change in EQ; with (|regs| = m) <EQ
    2626    @refl
    2727 ]
Note: See TracChangeset for help on using the changeset viewer.