some work

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 5263b84e40f137436e913ea4526e5b82d71027aa..27fbbb72cabe33b9cbfa74e0d299e95939132838 100755 (executable)
--- 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 ?)).