X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Flinearfe.ma;h=253127455844e38000e6e78f150a67d5275ec23d;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=1f264398b02375404015dba00562b18903acb9ec;hpb=92c1b82f32dd0db6af3cb1f56af23b78144fae9a;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/linearfe.ma b/helm/software/matita/contribs/assembly/compiler/linearfe.ma
index 1f264398b..253127455 100755
--- 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.
 
 (* -------------------------- *)