Changeset 3261 for src/LIN

Timestamp:

May 9, 2013, 11:12:07 AM (8 years ago)

Author:

piccolo

Message:

reverted joint_semantics rtl_semantics and ltl_semantics

File:

• src/LIN/joint_LTL_LIN_semantics.ma (modified) (2 diffs)

src/LIN/joint_LTL_LIN_semantics.ma

@@ -1 +1 @@
 include "LIN/joint_LTL_LIN.ma".
 include "joint/semanticsUtils.ma".
-
+ 
 definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
 definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
@@ -86 +86 @@
   (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
 *)  (* save_frame         ≝ *) LTL_LIN_save_frame
-  (* setup_call         ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.return st)
+  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
   (* fetch_external_args≝ *) ltl_lin_fetch_external_args
   (* set_result         ≝ *) ltl_lin_set_result