]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/tests/aliases.txt
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / ocaml / cic_disambiguation / tests / aliases.txt
diff --git a/helm/ocaml/cic_disambiguation/tests/aliases.txt b/helm/ocaml/cic_disambiguation/tests/aliases.txt
deleted file mode 100644 (file)
index 12b09ff..0000000
+++ /dev/null
@@ -1,6 +0,0 @@
-alias id foo = cic:/a.con
-alias id bar = cic:/b.con
-alias symbol "plus" (instance 0) = "real plus"
-alias symbol "plus" (instance 1) = "natural plus"
-alias num (instance 0) = "real number"
-alias num (instance 1) = "natural number"