mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly / compiler / preast_tree.ma

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma
old mode 100755 (executable)
new mode 100644 (file)
index 5263b84..aa11418
--- a/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -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 ?)).