Changeset 1599 for src/joint


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (9 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEGlobalenvs.ma

    r1408 r1599  
    447447      let 〈id, r, init〉 ≝ id_init in
    448448      let 〈g,st〉 ≝ g_st in
    449         match alloc_init_data st init r with [ pair st' b ⇒
     449      let 〈st',b〉 ≝ alloc_init_data st init r in
    450450          let g' ≝ add_symbol ? id b g in
    451451            〈g', st'〉
    452         ] )
     452    )
    453453    init_env vars.
    454454
  • src/joint/TranslateUtils.ma

    r1521 r1599  
    2121 #pars0 #globals #def #n elim n
    2222  [ %
    23   | #m whd in ⊢ (? → ??(??%)?); whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) ;
    24     cases (fresh_regs pars0 globals def m) normalize nodelta
    25     #def' #regs #EQ change with (|regs| = m)in EQ; <EQ
    26     @refl
    27  ]
     23  | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
     24    #def' #regs #EQ >EQ  normalize // ]
    2825qed.
    2926
Note: See TracChangeset for help on using the changeset viewer.