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

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

diff --git a/helm/gTopLevel/tests/match06.cic.test b/helm/gTopLevel/tests/match06.cic.test
deleted file mode 100644 (file)
index 0410956..0000000
--- a/helm/gTopLevel/tests/match06.cic.test
+++ /dev/null
@@ -1,19 +0,0 @@
-\lambda x:False.
-  [\lambda h:False. True]
-  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
-### (* METASENV after disambiguation  *)
-
-### (* TERM after disambiguation      *)
-[x:False]
-<[h:False]True>Cases x of 
-end
-### (* TYPE_OF the disambiguated term *)
-(x:False)([h:False]True x)
-### (* REDUCED disambiguated term     *)
-[x:False]
-<[h:False]True>Cases x of 
-end