ocaml 3.09 transition

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

diff --git a/helm/gTopLevel/tests/match05.cic.test b/helm/gTopLevel/tests/match05.cic.test
index 0c77d5dc41bcfd59cbbdb0bdad7b6e584b3095ab..1e80b5748a0a43a2295617babc0a919f8678e0c9 100644 (file)
--- a/helm/gTopLevel/tests/match05.cic.test
+++ b/helm/gTopLevel/tests/match05.cic.test
@@ -4,16 +4,16 @@ match nil:list with
 | (cons x y) \Rightarrow (cons x y) ]
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id cons = cic:/CoRN/algebra/ListType/list.ind#1/1/2
-alias id list = cic:/CoRN/algebra/ListType/list.ind#1/1
-alias id nil = cic:/CoRN/algebra/ListType/list.ind#1/1/1
+alias id cons = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1/2)
+alias id list = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1)
+alias id nil = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1/1)
 ### (* METASENV after disambiguation  *)
 _ :? _; _ :? _ |- ?25: Type
 ### (* 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[_ ; _]})
@@ -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[_ ; _]})