]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/tests/match06.cic.test
moved some old stuff to the history
[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 eb134e4..0000000
+++ /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#xpointer(1/1)
-alias id True = cic:/Coq/Init/Logic/True.ind#xpointer(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