Changeset 2512


Ignore:
Timestamp:
Dec 1, 2012, 8:36:52 PM (7 years ago)
Author:
mckinna
Message:

Simplified dependencies on ASM, to allow rollback to when AssmeblyProof?.ma checked.
But still a problem with disambiguation in ASM/AssemblyProofSplit.ma, starting from case 12: (* JC *) (l.1148). What's gone wrong?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2508 r2512  
    3535          lin_to_asm p.
    3636
    37 include "ASM/Fetch.ma". (* minimum needed for axiom to typecheck *)
     37(* JHM: minimum needed for assembler axiom to typecheck *)
     38(* JHM: moved from ASMCostsSplit.ma                     *)
     39(* JHM: should move elsewhere in ASM/                   *)
     40definition object_code ≝ list Byte.
     41definition costlabel_map ≝ BitVectorTrie costlabel 16.
    3842
    3943axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
     
    5559qed.
    5660*)
    57 
    5861
    5962include "ASM/ASMCosts.ma".
Note: See TracChangeset for help on using the changeset viewer.