freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / memory_abs.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
index 8e9f08c055b16b85a40fea3e3aab1853130771c7..17cadf037721658611ac9029e22894fded4b6c43 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
@@ -34,18 +34,6 @@ ninductive memory_impl : Type ≝
 | MEM_TREE: memory_impl
 | MEM_BITS: memory_impl.
 
-(*ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
-λP:memory_impl → Prop.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
- match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
-
-ndefinition memory_impl_rec : ΠP:memory_impl → Set.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
-λP:memory_impl → Set.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
- match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
-
-ndefinition memory_impl_rect : ΠP:memory_impl → Type.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
-λP:memory_impl → Type.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
- match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].*)
-
 (* ausiliario per il tipo della memoria *)
 ndefinition aux_mem_type ≝
 λt:memory_impl.match t with