Changeset 1902 for src/common

Timestamp:

Apr 26, 2012, 4:20:32 PM (8 years ago)

Author:

mulligan

Message:

Reverted needless changes to StructuredTraces?

File:

• src/common/StructuredTraces.ma (modified) (4 diffs)

src/common/StructuredTraces.ma

@@ -15 +15 @@
   as_classifier : as_status → status_class → Prop;
   as_costed : as_status → Prop;
-  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop;
-  as_program_counters_properly_related: as_status → as_status → Prop
+  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
 }.
 
@@ -71 +70 @@
           trace_label_return S status_start_fun_call status_final →
           as_costed S status_final →
-          as_program_counters_properly_related S status_pre_fun_call status_final →
             trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
   (* A call followed by a non-empty trace. *)
@@ -85 +83 @@
           trace_label_return S status_start_fun_call status_after_fun_call →
           ¬ as_costed S status_after_fun_call →
-          as_program_counters_properly_related S status_pre_fun_call status_after_fun_call →
           trace_any_label S end_flag status_after_fun_call status_final →
             trace_any_label S end_flag status_pre_fun_call status_final
@@ -219 +216 @@
 [ tal_base_not_return start final _ _ C ⇒ C
 | tal_base_return _ _  _ _ ⇒ I
-| tal_base_call _ _ _ _ _ _ _ C _ ⇒ C
-| tal_step_call f pre start after final X C RET PROPER LR C' tr' ⇒ trace_any_label_label … tr'
+| tal_base_call _ _ _ _ _ _ _ C ⇒ C
+| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
 | tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
 ].