This commit was manufactured by cvs2svn to create branch 'moogle'.

[helm.git] / helm / gTopLevel / tests / forall00.cic.test

diff --git a/helm/gTopLevel/tests/forall00.cic.test b/helm/gTopLevel/tests/forall00.cic.test
deleted file mode 100644 (file)
index 29a0644..0000000
--- a/helm/gTopLevel/tests/forall00.cic.test
+++ /dev/null
@@ -1,14 +0,0 @@
-\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 symbol "eq" (instance 0) = "leibnitz's equality"
-alias symbol "plus" (instance 0) = "natural plus"
-### (* METASENV after disambiguation  *)
-
-### (* TERM after disambiguation      *)
-(n:nat)(m:nat)(eq nat (plus n m) n)
-### (* TYPE_OF the disambiguated term *)
-Prop
-### (* REDUCED disambiguated term     *)
-(n:nat)(m:nat)(eq nat (plus n m) n)