mod change (-x)

[helm.git] / helm / software / matita / contribs / assembly / compiler / linearfe.ma

diff --git a/helm/software/matita/contribs/assembly/compiler/linearfe.ma b/helm/software/matita/contribs/assembly/compiler/linearfe.ma
old mode 100755 (executable)
new mode 100644 (file)
index 1f26439..2531274
--- a/helm/software/matita/contribs/assembly/compiler/linearfe.ma
+++ b/helm/software/matita/contribs/assembly/compiler/linearfe.ma
@@ -26,10 +26,12 @@ include "compiler/astfe_tree.ma".
 (* SUCCESSIONE APPIATITA DI ASSEGNAMENTI SU FLATENV *)
 (* ************************************************ *)
 
+inductive jumpNLabel : Type ≝
+  N_LABEL: nat → jumpNLabel.
+
 inductive jumpLabel : Type ≝
-  BEGIN_LABEL: jumpLabel
-| N_LABEL: nat → jumpLabel
-| END_LABEL: jumpLabel.
+  LABEL_N: jumpNLabel → jumpLabel
+| LABEL_END: jumpLabel.
 
 (* 
    L1 := goto L1
@@ -47,7 +49,7 @@ inductive linearfe_stm (e:aux_flatEnv_type) : Type ≝
 
 (* LABEL + [ init/assegnamenti ] + if(EXPR) then { goto LABEL; } else { goto LABEL; } *)
 inductive linearfe_elem (e:aux_flatEnv_type) : Type ≝
- LINEARFE_ELEM: jumpLabel → list (linearfe_stm e) → jumpBlock e → linearfe_elem e.
+ LINEARFE_ELEM: jumpNLabel → list (linearfe_stm e) → jumpBlock e → linearfe_elem e.
 
 (* -------------------------- *)