Changeset 2638 for src/ERTLptr


Ignore:
Timestamp:
Feb 7, 2013, 2:15:51 PM (7 years ago)
Author:
piccolo
Message:

Back-end fixes for last Garnier's commit that removes the regions from
the blocks. Only part of the back-end has been fixed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2604 r2638  
    12791279  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    12801280    bl = Error … [MSG BadFunction].
    1281  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     1281 #F#V#i#p ** #r #id #EQ1 destruct
    12821282  whd in match fetch_function; normalize nodelta
    12831283  >globalenv_no_minus_one
     
    12901290  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    12911291    bl = Error … [MSG BadFunction].
    1292  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     1292 #F#V#i#p ** #r #id #EQ1 destruct
    12931293  whd in match fetch_function; normalize nodelta
    12941294  >globalenv_no_zero
Note: See TracChangeset for help on using the changeset viewer.