ported to new xpointer syntax

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
index 8719cbed32ebf6bbcbcb9cdb08422d3f06c70595..8b3e333b82f46fe0863bbabd3b114dc6934a7b92 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  *)
 

diff --git a/helm/gTopLevel/tests/forall00.cic.test b/helm/gTopLevel/tests/forall00.cic.test
index 29a06443bd509a8c6ef6829579e03311d81a146b..fccef764ea7a673116429fa0d8aea0d264161783 100644 (file)
--- a/helm/gTopLevel/tests/forall00.cic.test
+++ b/helm/gTopLevel/tests/forall00.cic.test
@@ -1,7 +1,7 @@
 \forall n:nat. \forall m. n + m = n
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
 alias symbol "eq" (instance 0) = "leibnitz's equality"
 alias symbol "plus" (instance 0) = "natural plus"
 ### (* METASENV after disambiguation  *)

diff --git a/helm/gTopLevel/tests/lambda01.cic.test b/helm/gTopLevel/tests/lambda01.cic.test
index 4ca229fa8dbd693901b906ee6d2cc5d68b8627b6..6140de0b172be943097ccc687a20f1dbb6d5a1df 100644 (file)
--- a/helm/gTopLevel/tests/lambda01.cic.test
+++ b/helm/gTopLevel/tests/lambda01.cic.test
@@ -2,9 +2,9 @@
   \lambda n. \lambda H. (refl_equal nat 0))
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
-alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#1/1/1
+alias id le_n = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
+alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)
 alias num (instance 0) = "natural number"
 ### (* METASENV after disambiguation  *)
 

diff --git a/helm/gTopLevel/tests/lambda02.cic.test b/helm/gTopLevel/tests/lambda02.cic.test
index 259140c9ef6253ce02211d430b6dce0f34a5c960..2d813315c3aae8c6a5fd38671239b18d04c3d119 100644 (file)
--- a/helm/gTopLevel/tests/lambda02.cic.test
+++ b/helm/gTopLevel/tests/lambda02.cic.test
@@ -1,9 +1,9 @@
 \lambda f:(\forall n:nat. (\forall H:(le 0 n). (n=n))). (f 0 (le_n 0))
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id le = cic:/Coq/Init/Peano/le.ind#1/1
-alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id le = cic:/Coq/Init/Peano/le.ind#xpointer(1/1)
+alias id le_n = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
 alias num (instance 0) = "natural number"
 alias symbol "eq" (instance 0) = "leibnitz's equality"
 ### (* METASENV after disambiguation  *)

diff --git a/helm/gTopLevel/tests/lambda03.cic.test b/helm/gTopLevel/tests/lambda03.cic.test
index 4f21c833992db99fbb65e1daa29b6929ff75caaf..6ae0213b1d244ef94eb8921b2e29fffb841b2f2d 100644 (file)
--- a/helm/gTopLevel/tests/lambda03.cic.test
+++ b/helm/gTopLevel/tests/lambda03.cic.test
@@ -2,9 +2,9 @@
  \lambda H:n=n.\lambda g:(?\to (le n 0))\to True.(g \lambda f.(f n H))
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id True = cic:/Coq/Init/Logic/True.ind#1/1
-alias id le = cic:/Coq/Init/Peano/le.ind#1/1
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id True = cic:/Coq/Init/Logic/True.ind#xpointer(1/1)
+alias id le = cic:/Coq/Init/Peano/le.ind#xpointer(1/1)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
 alias num (instance 0) = "natural number"
 alias symbol "eq" (instance 0) = "leibnitz's equality"
 ### (* METASENV after disambiguation  *)

diff --git a/helm/gTopLevel/tests/match00.cic.test b/helm/gTopLevel/tests/match00.cic.test
index b2de9dbd117d276058e23800302d00672257dc80..28a4a412fcac7465facb70866cf42f63efc950b1 100644 (file)
--- a/helm/gTopLevel/tests/match00.cic.test
+++ b/helm/gTopLevel/tests/match00.cic.test
@@ -6,11 +6,11 @@ match (S O):nat with
 | (S x) \Rightarrow false ]
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
-alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
-alias id bool = cic:/Coq/Init/Datatypes/bool.ind#1/1
-alias id false = cic:/Coq/Init/Datatypes/bool.ind#1/1/2
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id O = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
+alias id bool = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)
+alias id false = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match01.cic.test b/helm/gTopLevel/tests/match01.cic.test
index 8d734e28f271491a98bbb3d095f106690fa26fab..13fbce756b613e620a10a38d8ceec5a1452d3120 100644 (file)
--- a/helm/gTopLevel/tests/match01.cic.test
+++ b/helm/gTopLevel/tests/match01.cic.test
@@ -4,12 +4,12 @@ match (le_n O): le with
 | (le_S x y) \Rightarrow (refl_equal nat O) ]
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
-alias id eq = cic:/Coq/Init/Logic/eq.ind#1/1
-alias id le = cic:/Coq/Init/Peano/le.ind#1/1
-alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
-alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#1/1/1
+alias id O = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)
+alias id eq = cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)
+alias id le = cic:/Coq/Init/Peano/le.ind#xpointer(1/1)
+alias id le_n = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
+alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match02.cic.test b/helm/gTopLevel/tests/match02.cic.test
index 49f680053b51fe6ba23ab97226b4e7d0497d5485..08a583805b63fa8cd05bd5709678a067e5bea9df 100644 (file)
--- a/helm/gTopLevel/tests/match02.cic.test
+++ b/helm/gTopLevel/tests/match02.cic.test
@@ -4,11 +4,11 @@ match (le_S 0 0 (le_n 0)): le with
 | (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
-alias id le = cic:/Coq/Init/Peano/le.ind#1/1
-alias id le_S = cic:/Coq/Init/Peano/le.ind#1/1/2
-alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
+alias id le = cic:/Coq/Init/Peano/le.ind#xpointer(1/1)
+alias id le_S = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/2)
+alias id le_n = cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
 alias num (instance 0) = "natural number"
 ### (* METASENV after disambiguation  *)
 

diff --git a/helm/gTopLevel/tests/match03.cic.test b/helm/gTopLevel/tests/match03.cic.test
index 94681ed5962b1910183d5d45e47ea7ccb67a6bab..bc5db2d042fd26b08722cb853e99f0bbfc3c0b28 100644 (file)
--- a/helm/gTopLevel/tests/match03.cic.test
+++ b/helm/gTopLevel/tests/match03.cic.test
@@ -4,11 +4,11 @@ match true:bool with
 | false \Rightarrow (S O) ]
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
-alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
-alias id bool = cic:/Coq/Init/Datatypes/bool.ind#1/1
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
-alias id true = cic:/Coq/Init/Datatypes/bool.ind#1/1/1
+alias id O = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
+alias id bool = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
+alias id true = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match04.cic.test b/helm/gTopLevel/tests/match04.cic.test
index 9c8016c60056c18b3460f5022f76c7188f135e5e..8befe4c3dbbbbf93dfaffa16a5a0b0e41b9c7a93 100644 (file)
--- a/helm/gTopLevel/tests/match04.cic.test
+++ b/helm/gTopLevel/tests/match04.cic.test
@@ -4,9 +4,9 @@ match O:nat with
 | (S x) \Rightarrow (S (S x)) ]
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
-alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id O = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match05.cic.test b/helm/gTopLevel/tests/match05.cic.test
index 0c77d5dc41bcfd59cbbdb0bdad7b6e584b3095ab..0068d3a9e34c2dd716446142cafdbf9bf9cf348a 100644 (file)
--- a/helm/gTopLevel/tests/match05.cic.test
+++ b/helm/gTopLevel/tests/match05.cic.test
@@ -4,9 +4,9 @@ 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      *)

diff --git a/helm/gTopLevel/tests/match06.cic.test b/helm/gTopLevel/tests/match06.cic.test
index 0410956381d04f3099214fe854687e9ae4e57d7b..eb134e429a5bf557db2e84c3fe34717d70dac30a 100644 (file)
--- a/helm/gTopLevel/tests/match06.cic.test
+++ b/helm/gTopLevel/tests/match06.cic.test
@@ -3,8 +3,8 @@
   match x:False with []
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id False = cic:/Coq/Init/Logic/False.ind#1/1
-alias id True = cic:/Coq/Init/Logic/True.ind#1/1
+alias id False = cic:/Coq/Init/Logic/False.ind#xpointer(1/1)
+alias id True = cic:/Coq/Init/Logic/True.ind#xpointer(1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match07.cic.test b/helm/gTopLevel/tests/match07.cic.test
index a8331cff18379052a38e980065322012ef3d5617..690ccd28ab82fa1aac5bc2dffb09471473941669 100644 (file)
--- a/helm/gTopLevel/tests/match07.cic.test
+++ b/helm/gTopLevel/tests/match07.cic.test
@@ -4,11 +4,11 @@ match true with
 | false \Rightarrow (S O) ]
 ###### INTERPRETATION NUMBER 1 ######
 ### (* disambiguation environment  *)
-alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
-alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
-alias id bool = cic:/Coq/Init/Datatypes/bool.ind#1/1
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
-alias id true = cic:/Coq/Init/Datatypes/bool.ind#1/1/1
+alias id O = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
+alias id bool = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
+alias id true = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)