mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly2 / emulator / status / IP2022_status_base.ma

diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/status/IP2022_status_base.ma b/helm/software/matita/contribs/ng_assembly2/emulator/status/IP2022_status_base.ma
old mode 100755 (executable)
new mode 100644 (file)
index 340fafe..9cf4f2a
--- a/helm/software/matita/contribs/ng_assembly2/emulator/status/IP2022_status_base.ma
+++ b/helm/software/matita/contribs/ng_assembly2/emulator/status/IP2022_status_base.ma
@@ -76,11 +76,9 @@ unification hint 0 ≔ ⊢ carr callstack_is_comparable ≡ aux_callstack_type.
 ndefinition aux_addrarray_type ≝ Array8T word24.
 
 (* tutti a 0x000000 on reset *)
-ndefinition new_addrarray ≝
- mk_Array8T ? (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
-              (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
-              (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
-              (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
+ndefinition new_addrarray : aux_addrarray_type ≝
+ mk_Array8T ? (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
+              (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?).
 
 ndefinition get_addrarray ≝
 λaddrsel:byte8.λaa:aux_addrarray_type.