Changeset 1902 for src/common


Ignore:
Timestamp:
Apr 26, 2012, 4:20:32 PM (8 years ago)
Author:
mulligan
Message:

Reverted needless changes to StructuredTraces?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1901 r1902  
    1515  as_classifier : as_status → status_class → Prop;
    1616  as_costed : as_status → Prop;
    17   as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop;
    18   as_program_counters_properly_related: as_status → as_status → Prop
     17  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    1918}.
    2019
     
    7170          trace_label_return S status_start_fun_call status_final →
    7271          as_costed S status_final →
    73           as_program_counters_properly_related S status_pre_fun_call status_final →
    7472            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
    7573  (* A call followed by a non-empty trace. *)
     
    8583          trace_label_return S status_start_fun_call status_after_fun_call →
    8684          ¬ as_costed S status_after_fun_call →
    87           as_program_counters_properly_related S status_pre_fun_call status_after_fun_call →
    8885          trace_any_label S end_flag status_after_fun_call status_final →
    8986            trace_any_label S end_flag status_pre_fun_call status_final
     
    219216[ tal_base_not_return start final _ _ C ⇒ C
    220217| tal_base_return _ _  _ _ ⇒ I
    221 | tal_base_call _ _ _ _ _ _ _ C _ ⇒ C
    222 | tal_step_call f pre start after final X C RET PROPER LR C' tr' ⇒ trace_any_label_label … tr'
     218| tal_base_call _ _ _ _ _ _ _ C ⇒ C
     219| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
    223220| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
    224221].
Note: See TracChangeset for help on using the changeset viewer.