From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 29 Nov 2004 12:31:21 +0000 (+0000)
Subject: - ported tests to newer PP / substitutions
X-Git-Tag: PRE_UNIVERSES~2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3165714b1155d36e651ff9bcc86c1b49144fb07b;p=helm.git

- ported tests to newer PP / substitutions
---

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
diff --git a/helm/gTopLevel/tests/lambda03.cic b/helm/gTopLevel/tests/lambda03.cic
index f67c4bd99..0279eeecc 100644
--- 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 0068d3a9e..1e80b5748 100644
--- 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[_ ; _]})