Changeset 2763 for src/compiler.ma


Ignore:
Timestamp:
Mar 2, 2013, 11:42:16 AM (8 years ago)
Author:
sacerdot
Message:

All daemons in compiler.ma closed (i.e. proof obligations added
to the sigma type of compiled programs).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2762 r2763  
    5757  let pol ≝ λppc. \snd sigma_pol ppc in
    5858  OK ? (assembly p sigma pol).
    59   cases daemon
    60 qed.
    6159
    6260include "ASM/ASMCosts.ma".
Note: See TracChangeset for help on using the changeset viewer.