ocaml 3.09 transition

[helm.git] / helm / gTopLevel / tests / fix00.cic.test

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
index 8719cbed32ebf6bbcbcb9cdb08422d3f06c70595..c3a4cfcd2380fafe4fa3f0cef929060398ac4433 100644 (file)
--- a/helm/gTopLevel/tests/fix00.cic.test
+++ b/helm/gTopLevel/tests/fix00.cic.test
@@ -8,9 +8,9 @@ in
 (fact 4)
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
 alias id mult = cic:/Coq/Init/Peano/mult.con
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
 alias num (instance 0) = "natural number"
 ### (* METASENV after disambiguation  *)
 
@@ -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