- setters for data structures now support "commuting conversion"-like

[helm.git] / helm / software / matita / contribs / assembly / compiler / preast_to_ast.ma

diff --git a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
index 141544c33b45a29a2910590582694c8c8878b66b..49a027ba7d18e951365c04bc47f5fe831909d743 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
@@ -385,7 +385,7 @@ definition preast_to_ast_init_val_aux_array :
 λt:ast_type.λn:nat.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)).x.
 
 definition preast_to_ast_init_val_aux_struct :
-Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («t£»&nel))) ≝
+Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («£t»&nel))) ≝
 λt:ast_type.λnel:ne_list ast_type.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)).x.
 
 let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt.aux_ast_init_type t) ≝
@@ -439,7 +439,7 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (
      [ ne_nil h ⇒
       opt_map ?? (preast_to_ast_init_val_aux h)
        (λsigmaRes:(Σt.aux_ast_init_type t).match sigmaRes with [ sigma_intro t res ⇒
-        Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT (« t £»)),res≫ ])
+        Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t»)),res≫ ])
      | ne_cons h tl ⇒ 
       opt_map ?? (preast_to_ast_init_val_aux h)
        (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
@@ -452,7 +452,7 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (
               return λx.(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = x) → option (Σt.aux_ast_init_type t)
              with
               [ true ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = true).
-               Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («t1£»&nelSubType)),
+               Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t1»&nelSubType)),
                                               (preast_to_ast_init_val_aux_struct ??
                                                (pair (aux_ast_init_type t1) (aux_ast_init_type (AST_TYPE_STRUCT nelSubType))
                                                      res1
@@ -517,7 +517,7 @@ let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : optio
    opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) e)
                                      (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (enter_env e))
                                       (λresDecl.opt_map ?? t
-                                       (λt'.Some ? («(pair ?? resExpr resDecl)£»&t')))))
+                                       (λt'.Some ? («£(pair ?? resExpr resDecl)»&t')))))
                                     (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 e 〈x0,x0〉)) (AST_NO_DECL (enter_env e) (nil ?)))))
                                     nelExprDecl)
     (λres.match optDecl with
@@ -570,7 +570,7 @@ PREAST_ROOT (
  PREAST_DECL true [ ch_Q ] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (None ?) (
   PREAST_NO_DECL [
    PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x0,x0〉) (
-    PREAST_DECL false [ ch_P ] (AST_TYPE_STRUCT «(AST_TYPE_BASE AST_BASE_TYPE_BYTE8)£(AST_TYPE_BASE AST_BASE_TYPE_WORD16)») (None ?) (
+    PREAST_DECL false [ ch_P ] (AST_TYPE_STRUCT «(AST_TYPE_BASE AST_BASE_TYPE_WORD16)£(AST_TYPE_BASE AST_BASE_TYPE_BYTE8)») (None ?) (
      PREAST_NO_DECL [
       PREAST_STM_ASG (PREAST_VAR_STRUCT (PREAST_VAR_ID [ ch_P ]) 1) (PREAST_EXPR_ID (PREAST_VAR_ARRAY (PREAST_VAR_ID [ ch_Q ]) (PREAST_EXPR_BYTE8 〈x0,x1〉))) 
      ]