X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftests%2Fmatch05.cic.test;h=1e80b5748a0a43a2295617babc0a919f8678e0c9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0068d3a9e34c2dd716446142cafdbf9bf9cf348a;hpb=c67937ec06d9f7914b9f863e1afb2e4a7e489161;p=helm.git

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[_ ; _]})