]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/tests/match05.cic.test
first moogle template checkin
[helm.git] / helm / gTopLevel / tests / match05.cic.test
index 921264d6ac04b1607d34d4c168a669e912107b0c..0c77d5dc41bcfd59cbbdb0bdad7b6e584b3095ab 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:/Algebra/algebra/ListType/list.ind#1/1/2
-alias id list = cic:/Algebra/algebra/ListType/list.ind#1/1
-alias id nil = cic:/Algebra/algebra/ListType/list.ind#1/1/1
+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
 ### (* METASENV after disambiguation  *)
 _ :? _; _ :? _ |- ?25: Type
 ### (* TERM after disambiguation      *)