X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftests%2Ffix00.cic.test;h=c3a4cfcd2380fafe4fa3f0cef929060398ac4433;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=8b3e333b82f46fe0863bbabd3b114dc6934a7b92;hpb=c67937ec06d9f7914b9f863e1afb2e4a7e489161;p=helm.git

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
index 8b3e333b8..c3a4cfcd2 100644
--- a/helm/gTopLevel/tests/fix00.cic.test
+++ b/helm/gTopLevel/tests/fix00.cic.test
@@ -29,7 +29,7 @@ nat
 ### (* REDUCED disambiguated term     *)
 (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -37,7 +37,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -45,7 +45,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -53,7 +53,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -61,7 +61,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -69,7 +69,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -77,7 +77,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -85,7 +85,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -93,7 +93,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -101,7 +101,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -109,7 +109,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -117,7 +117,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -125,7 +125,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -133,7 +133,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -141,7 +141,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -149,7 +149,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -157,7 +157,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -165,7 +165,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -173,7 +173,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -181,7 +181,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -189,7 +189,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -197,7 +197,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -205,7 +205,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -213,7 +213,7 @@ plus / 0 : (n:nat)(m:nat)nat :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(m:nat)nat := 
+plus / 0 : (nat->(nat->nat)) := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m