X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftests%2Fmatch04.cic.test;fp=helm%2FgTopLevel%2Ftests%2Fmatch04.cic.test;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=9c8016c60056c18b3460f5022f76c7188f135e5e;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git

diff --git a/helm/gTopLevel/tests/match04.cic.test b/helm/gTopLevel/tests/match04.cic.test
deleted file mode 100644
index 9c8016c60..000000000
--- a/helm/gTopLevel/tests/match04.cic.test
+++ /dev/null
@@ -1,21 +0,0 @@
-[\lambda x:nat. nat]
-match O:nat with
-[ O \Rightarrow O
-| (S x) \Rightarrow (S (S x)) ]
-###### INTERPRETATION NUMBER 1 ######
-### (* disambiguation environment  *)
-alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
-alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
-### (* METASENV after disambiguation  *)
-
-### (* TERM after disambiguation      *)
-
-<[x:nat]nat>Cases O of 
- O => O
- S => [x:nat](S (S x))
-end
-### (* TYPE_OF the disambiguated term *)
-([x:nat]nat O)
-### (* REDUCED disambiguated term     *)
-O