X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fpreast_tree.ma;h=27fbbb72cabe33b9cbfa74e0d299e95939132838;hb=8134330933e377a344b5ee38890198dc0b653428;hp=5263b84e40f137436e913ea4526e5b82d71027aa;hpb=38fccc2b774e493a94eedef76342b56079c0e694;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma
index 5263b84e4..27fbbb72c 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma
@@ -73,7 +73,7 @@ with preast_var : Type ≝
 (* -------------------------- *)
 
 (* inizializzatori: ... valori ... *)
-inductive preast_init_val : Type ≝
+ninductive preast_init_val : Type ≝
   PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
 | PREAST_INIT_VAL_WORD16: word16 → preast_init_val
 | PREAST_INIT_VAL_WORD32: word32 → preast_init_val
@@ -85,17 +85,17 @@ inductive preast_init_val : Type ≝
   1) var1 = var2
   2) var = ... valori ...
 *)
-inductive preast_init : Type ≝
+ninductive preast_init : Type ≝
   PREAST_INIT_VAR: preast_var → preast_init
 | PREAST_INIT_VAL: preast_init_val → preast_init.
 
 (* -------------------------- *)
 
 (* statement: assegnamento/while/if else if else *)
-inductive preast_stm : Type ≝
+ninductive preast_stm : Type ≝
   PREAST_STM_ASG: preast_var → preast_expr → preast_stm
 | PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
-| PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
+| PREAST_STM_IF: ne_list (ProdT preast_expr preast_decl) → option preast_decl → preast_stm
 
 (* dichiarazioni *)
 with preast_decl : Type ≝
@@ -106,10 +106,10 @@ with preast_decl : Type ≝
 (* -------------------------- *)
 
 (* programma *)
-inductive preast_root : Type ≝
+ninductive preast_root : Type ≝
   PREAST_ROOT: preast_decl → preast_root.
 
 (* -------------------------- *)
 
 (* programma vuoto *)
-definition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).
+ndefinition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).