Ignore:
Timestamp:
Jan 5, 2013, 1:41:13 PM (7 years ago)
Author:
piccolo
Message:

ERTLtoERTLptr in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2564 r2570  
    55include "joint/Joint.ma".
    66include "ASM/I8051bis.ma".
    7 (* include "common/extraGlobalenvs.ma". *)
     7include "common/extraGlobalenvs.ma".
    88
    99(* CSC: external functions never fail (??) and always return something of the
     
    151151 | _ ⇒ Error … [MSG BadFunction]
    152152 ].
     153 
     154lemma fetch_internal_function_no_minus_one :
     155  ∀F,V,i,p,bl.
     156  block_id (pi1 … bl) = -1 →
     157  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
     158    bl = Error … [MSG BadFunction].
     159 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     160 whd in match fetch_internal_function;
     161  whd in match fetch_function; normalize nodelta
     162  >globalenv_no_minus_one
     163  cases (symbol_for_block ???) normalize //
     164qed.
    153165
    154166inductive call_kind : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.