- ported tests to newer PP / substitutions

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
index 8b3e333b82f46fe0863bbabd3b114dc6934a7b92..c3a4cfcd2380fafe4fa3f0cef929060398ac4433 100644 (file)
--- 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

diff --git a/helm/gTopLevel/tests/lambda03.cic b/helm/gTopLevel/tests/lambda03.cic
index f67c4bd991f6102d92386922371a4faa45cbb7c2..0279eeecc5b21e6092e0adeaaa051a6ea46624ec 100644 (file)
--- a/helm/gTopLevel/tests/lambda03.cic
+++ b/helm/gTopLevel/tests/lambda03.cic
@@ -1,2 +1,3 @@
 \lambda n:nat.
- \lambda H:n=n.\lambda g:(?\to (le n 0))\to True.(g \lambda f.(f n H))
+ \lambda H:n=n.
+  \lambda g:(?\to (le n 0))\to True.(g (\lambda f.(f n H)))

diff --git a/helm/gTopLevel/tests/match05.cic.test b/helm/gTopLevel/tests/match05.cic.test
index 0068d3a9e34c2dd716446142cafdbf9bf9cf348a..1e80b5748a0a43a2295617babc0a919f8678e0c9 100644 (file)
--- a/helm/gTopLevel/tests/match05.cic.test
+++ b/helm/gTopLevel/tests/match05.cic.test
@@ -13,7 +13,7 @@ _ :? _; _ :? _ |- ?25: Type
 
 <[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of 
  nil => nil{A:=?25[_ ; _]}
- cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
+ cons => [x:?25[_ ; _]][y:list{A:=?25[_ ; x]}](cons{A:=?25[x ; y]} x y)
 end
 ### (* TYPE_OF the disambiguated term *)
 ([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
@@ -21,16 +21,16 @@ end
 nil{A:=?25[_ ; _]}
 ###### INTERPRETATION NUMBER 2 ######
 ### (* disambiguation environment  *)
-alias id cons = cic:/Coq/Lists/List/list.ind#1/1/2
-alias id list = cic:/Coq/Lists/List/list.ind#1/1
-alias id nil = cic:/Coq/Lists/List/list.ind#1/1/1
+alias id cons = cic:/Coq/Lists/List/list.ind#xpointer(1/1/2)
+alias id list = cic:/Coq/Lists/List/list.ind#xpointer(1/1)
+alias id nil = cic:/Coq/Lists/List/list.ind#xpointer(1/1/1)
 ### (* METASENV after disambiguation  *)
 _ :? _; _ :? _ |- ?25: Set
 ### (* TERM after disambiguation      *)
 
 <[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of 
  nil => nil{A:=?25[_ ; _]}
- cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
+ cons => [x:?25[_ ; _]][y:list{A:=?25[_ ; x]}](cons{A:=?25[x ; y]} x y)
 end
 ### (* TYPE_OF the disambiguated term *)
 ([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
@@ -38,9 +38,9 @@ end
 nil{A:=?25[_ ; _]}
 ###### INTERPRETATION NUMBER 3 ######
 ### (* disambiguation environment  *)
-alias id cons = cic:/Coq/Lists/MonoList/list.ind#1/1/2
-alias id list = cic:/Coq/Lists/MonoList/list.ind#1/1
-alias id nil = cic:/Coq/Lists/MonoList/list.ind#1/1/1
+alias id cons = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1/2)
+alias id list = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1)
+alias id nil = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)
@@ -55,16 +55,16 @@ end
 nil
 ###### INTERPRETATION NUMBER 4 ######
 ### (* disambiguation environment  *)
-alias id cons = cic:/Lannion/continuations/weight/specif/list.ind#1/1/2
-alias id list = cic:/Lannion/continuations/weight/specif/list.ind#1/1
-alias id nil = cic:/Lannion/continuations/weight/specif/list.ind#1/1/1
+alias id cons = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1/2)
+alias id list = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1)
+alias id nil = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1/1)
 ### (* METASENV after disambiguation  *)
 _ :? _; _ :? _ |- ?25: Set
 ### (* TERM after disambiguation      *)
 
 <[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of 
  nil => nil{A:=?25[_ ; _]}
- cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
+ cons => [x:?25[_ ; _]][y:list{A:=?25[_ ; x]}](cons{A:=?25[x ; y]} x y)
 end
 ### (* TYPE_OF the disambiguated term *)
 ([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})