Smaller formulae.

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

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
index 1fa93ce72fc55c6f173c03d369da4610603dfcc4..828e7ffc4a83970e193be630469376fdd43059db 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
@@ -21,7 +21,6 @@
 (* ********************************************************************** *)
 
 include "utility/utility.ma".
-include "freescale/nat_lemmas.ma".
 
 (* ************************* *)
 (* dimensioni degli elementi *)
@@ -136,5 +135,5 @@ nlet rec eval_size_type (ast:ast_type) on ast ≝
  match ast with
   [ AST_TYPE_BASE b ⇒ eval_size_base_type b
   | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
-  | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast
+  | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList … (λt,x.(eval_size_type t)+x) O nel_ast
   ].