Changeset 1378 for src/LTL/LTL.ma

Timestamp:

Oct 14, 2011, 7:32:21 PM (9 years ago)

Author:

sacerdot

Message:

New file LIN/joint_LTL_LIN.ma to factorize out the syntactic parameters shared
by LTL and LIN.

File:

• src/LTL/LTL.ma (modified) (1 diff)

src/LTL/LTL.ma

@@ -1 @@
-include "joint/Joint.ma".
+include "LIN/joint_LTL_LIN.ma".
 
-definition ltl_params__: params__ ≝
- (mk_params__ unit unit unit unit registers_move Register nat unit False).
-definition ltl_params_ : params_ ≝ graph_params_ ltl_params__.
-definition ltl_params0 : params0 ≝ mk_params0 ltl_params__ unit unit.
-definition ltl_params1 : params1 ≝ mk_params1 ltl_params0 unit.
-definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params1.
+definition ltl_params_ : params_ ≝ graph_params_ ltl_lin_params__.
+definition ltl_params: ∀globals. params globals ≝ graph_params ltl_lin_params1.
 
 definition ltl_statement ≝ joint_statement ltl_params_.
-
 definition ltl_program ≝ joint_program ltl_params.