1) PTS simplified

[helm.git] / helm / software / matita / contribs / ng_assembly / utility / string.ma

diff --git a/helm/software/matita/contribs/ng_assembly/utility/string.ma b/helm/software/matita/contribs/ng_assembly/utility/string.ma
index d2a55290124d6b60ac9ba2a317c6daf21f1aca62..ea1c1ccd145b9e21d50a6ecb82b2f957eb5f53e0 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/utility/string.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/string.ma
@@ -51,7 +51,7 @@ nlet rec eq_str (str,str':aux_str_type) ≝
 ninductive aux_strId_type : Type ≝
  STR_ID: aux_str_type → nat → aux_strId_type.
 
-ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
+(*ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
 λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
  match a with [ STR_ID l n ⇒ f l n ].
 
@@ -61,7 +61,7 @@ ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n
 
 ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
 λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].
+ match a with [ STR_ID l n ⇒ f l n ].*)
 
 (* getter *)
 ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].