From: Stefano Zacchiroli 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 *)