From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 26 Nov 2004 14:17:01 +0000 (+0000)
Subject: ported to new xpointer syntax
X-Git-Tag: PRE_UNIVERSES~11
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c67937ec06d9f7914b9f863e1afb2e4a7e489161;p=helm.git

ported to new xpointer syntax
---

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
index 8719cbed3..8b3e333b8 100644
--- 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 29a06443b..fccef764e 100644
--- 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 4ca229fa8..6140de0b1 100644
--- 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 259140c9e..2d813315c 100644
--- 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 4f21c8339..6ae0213b1 100644
--- 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 b2de9dbd1..28a4a412f 100644
--- 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 8d734e28f..13fbce756 100644
--- 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 49f680053..08a583805 100644
--- 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 94681ed59..bc5db2d04 100644
--- 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 9c8016c60..8befe4c3d 100644
--- 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 0c77d5dc4..0068d3a9e 100644
--- 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 041095638..eb134e429 100644
--- 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 a8331cff1..690ccd28a 100644
--- 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      *)