]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/tests/match05.cic.test
ported to new xpointer syntax
[helm.git] / helm / gTopLevel / tests / match05.cic.test
index 0c77d5dc41bcfd59cbbdb0bdad7b6e584b3095ab..0068d3a9e34c2dd716446142cafdbf9bf9cf348a 100644 (file)
@@ -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      *)