minor simplification + deps fixed

diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma
index 8b3b2623d8e84007aeee2060ecf4c89aad0481b6..f341480d7f4ac91a0d7a7edfee323dd8799c2fda 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma
+++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma
@@ -75,14 +75,20 @@ definition aux_map_type ≝ λd.list (map_elem d).
 
 definition empty_map ≝ nil (map_elem O).
 
-axiom defined_nList_S_to_true :
+theorem defined_nList_S_to_true :
 ∀d.∀l:n_list (S d).defined_nList (S d) l = True.
+ intros;
+ inversion l;
+  [ intros; destruct H
+  | intros; simplify; reflexivity
+  ]
+qed.
 
 lemma defined_get_id :
- ∀d.∀h:map_elem d.True → defined_nList (S d) (get_cur_mapElem d h).
- intros 3;
+ ∀d.∀h:map_elem d.defined_nList (S d) (get_cur_mapElem d h).
+ intros 2;
  rewrite > (defined_nList_S_to_true ? (get_cur_mapElem d h));
- apply H.
+ apply I.
 qed.
 
 (* get_id *)
@@ -90,7 +96,7 @@ let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : optio
  match map with
   [ nil ⇒ None ?
   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
-                [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ?? I)
+                [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??)
                 | false ⇒ get_id_map_aux d t name
                 ]
   ].
@@ -371,7 +377,7 @@ let rec enter_map d (map:aux_map_type d) on map ≝
              (get_name_mapElem d h)
              (get_max_mapElem d h)
              (n_cons (S d)
-                     (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ?? I))
+                     (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ??))
                      (get_cur_mapElem d h))
    )::(enter_map d t)
   ].
@@ -422,7 +428,7 @@ let rec leave_map d (map:aux_map_type (S d)) on map ≝
    (MAP_ELEM d
              (get_name_mapElem (S d) h)
              (get_max_mapElem (S d) h)
-             (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ?? I))
+             (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ??))
    )::(leave_map d t)
   ].
 
@@ -439,7 +445,7 @@ let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on
  match map with
   [ nil ⇒ []
   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
-                [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ?? I)))
+                [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??)))
                 | false ⇒ h
                 ]::(new_max_map_aux d t name max) 
   ].

diff --git a/helm/software/matita/contribs/assembly/depends b/helm/software/matita/contribs/assembly/depends
index 38db65f2f058dddee3d759259133db7adac9675b..103d25a7db85cdfce706d7dae46452e4cf3a0f14 100644 (file)
--- a/helm/software/matita/contribs/assembly/depends
+++ b/helm/software/matita/contribs/assembly/depends
@@ -9,6 +9,7 @@ freescale/extra.ma datatypes/constructors.ma list/list.ma logic/connectives.ma n
 freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma
 compiler/env_to_flatenv.ma compiler/environment.ma
 freescale/table_RS08.ma freescale/opcode.ma
+compiler/astfe_tree1.ma compiler/ast_tree.ma compiler/ast_type.ma compiler/env_to_flatenv1.ma compiler/utility.ma freescale/word32.ma string/string.ma
 freescale/memory_trees.ma freescale/memory_struct.ma
 freescale/table_HC05_tests.ma freescale/table_HC05.ma
 freescale/aux_bases.ma freescale/word16.ma
@@ -35,6 +36,7 @@ compiler/sigma.ma
 compiler/ast_to_astfe.ma compiler/astfe_tree.ma compiler/sigma.ma
 compiler/utility.ma freescale/extra.ma
 compiler/ast_type.ma compiler/utility.ma freescale/word32.ma
+compiler/ast_to_astfe1.ma compiler/astfe_tree1.ma compiler/sigma.ma
 compiler/preast_to_ast.ma compiler/ast_tree.ma compiler/preast_tree.ma compiler/sigma.ma
 freescale/translation.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
 freescale/byte8.ma freescale/exadecim.ma