Elimination principles are now processed in O(1) again

[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 8f6de6f4719186fac7edcfbb051022e2a07eabd8..d972fe0bae891b3de5e6a7949eb0dd42c37aca28 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
@@ -33,7 +33,7 @@ ninductive ast_base_type : Type ≝
 | AST_BASE_TYPE_WORD16: ast_base_type
 | AST_BASE_TYPE_WORD32: ast_base_type.
 
-ndefinition ast_base_type_ind
+(*ndefinition ast_base_type_ind
  : ΠP:ast_base_type → Prop.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
    Πa:ast_base_type.P a ≝
 λP:ast_base_type → Prop.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
@@ -53,7 +53,7 @@ ndefinition ast_base_type_rect
 λP:ast_base_type → Type.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
 λa:ast_base_type.
  match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
-
+*)
 ninductive ast_type : Type ≝
   AST_TYPE_BASE: ast_base_type → ast_type
 | AST_TYPE_ARRAY: ast_type → nat → ast_type
@@ -69,7 +69,7 @@ nlet rec ast_type_ind_aux (P:ast_type → Prop)
   | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_ind_aux P f f1 f2 t)
   ].
 
-nlet rec ast_type_ind (P:ast_type → Prop)
+(*nlet rec ast_type_ind (P:ast_type → Prop)
                       (f:Πb.P (AST_TYPE_BASE b))
                       (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
                       (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
@@ -84,7 +84,7 @@ nlet rec ast_type_ind (P:ast_type → Prop)
    ]
   ]. 
 
-nlet rec ast_type_rec_aux (P:ast_type → Set)
+nlet rec ast_type_rec_aux (P:ast_type → Type[0])
                           (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
                           (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
                           (f2:Πt.P t)
@@ -133,7 +133,7 @@ nlet rec ast_type_rect (P:ast_type → Type)
    | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t)
    ]
   ]. 
-
+*)
 ndefinition eq_ast_base_type ≝
 λt1,t2:ast_base_type.match t1 with
  [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with