Changeset 1071 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Jul 15, 2011, 2:40:40 PM (9 years ago)
Author:
mulligan
Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r878 r1071  
    2525  | ertl_st_int: register → Byte → label → ertl_statement
    2626  | ertl_st_move: register → register → label → ertl_statement
    27   | ertl_st_opaccs: OpAccs → register → register → register → label → ertl_statement
     27  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
     28  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
    2829  | ertl_st_op1: Op1 → register → register → label → ertl_statement
    2930  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    3031  | ertl_st_clear_carry: label → ertl_statement
     32  | ertl_st_set_carry: label → ertl_statement
    3133  | ertl_st_load: register → register → register → label → ertl_statement
    3234  | ertl_st_store: register → register → register → label → ertl_statement
    3335  | ertl_st_call_id: ident → Byte → label → ertl_statement
    34   | ertl_st_cond_acc: register → label → label → ertl_statement
    35   | ertl_st_return: registers → ertl_statement.
     36  | ertl_st_cond: register → label → label → ertl_statement
     37  | ertl_st_return: ertl_statement. (* XXX: change from o'caml *)
    3638
    3739definition ertl_statement_graph ≝ graph ertl_statement.
     
    4951}.
    5052
    51 inductive ertl_function: Type[0] ≝
    52   | ertl_f_internal: ertl_internal_function → ertl_function
    53   | ertl_f_external: external_function → ertl_function.
     53definition ertl_function ≝ fundef ertl_internal_function.
    5454 
    5555record ertl_program: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.