X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Ftests%2Fmatch.txt;fp=helm%2Focaml%2Fcic_disambiguation%2Ftests%2Fmatch.txt;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=87bb0159b72b93536b75569335780e84ecb43c4b;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/tests/match.txt b/helm/ocaml/cic_disambiguation/tests/match.txt
deleted file mode 100644
index 87bb0159b..000000000
--- a/helm/ocaml/cic_disambiguation/tests/match.txt
+++ /dev/null
@@ -1,49 +0,0 @@
-[\lambda x:nat.
-  [\lambda y:nat. Set]
-    match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
-match (S O):nat with
-[ O \Rightarrow O
-| (S x) \Rightarrow false ]
-
-[\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
-match (le_n O): le with
-[ le_n \Rightarrow (refl_equal nat O)
-| (le_S x y) \Rightarrow (refl_equal nat O) ]
-
-[\lambda z:nat. \lambda h:(le (plus (plus O O) (plus O O)) z). (eq nat (plus (plus O O) (plus O O)) (plus (plus O O) (plus O O)))]
-match (le_n (plus (plus O O) (plus O O))): le with
-[ le_n \Rightarrow (refl_equal nat (plus (plus O O) (plus O O)))
-| (le_S x y) \Rightarrow (refl_equal nat (plus (plus O O) (plus O O))) ]
-
-(*
-[\lambda z:nat. \lambda h:(le 1 z). (le 0 z)]
-match (le_S 2 (le_n 1)): le with
-[ le_n \Rightarrow (le_S 1 (le_n 0))
-| (le_S x y) \Rightarrow y ]
-*)
-
-[\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
-match (le_S 0 0 (le_n 0)): le with
-[ le_n \Rightarrow (le_S 0 0 (le_n 0))
-| (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
-
-
-[\lambda x:bool. nat]
-match true:bool with
-[ true \Rightarrow O
-| false \Rightarrow (S O) ]
-
-[\lambda x:nat. nat]
-match O:nat with
-[ O \Rightarrow O
-| (S x) \Rightarrow (S (S x)) ]
-
-[\lambda x:list. list]
-match nil:list with
-[ nil \Rightarrow nil
-| (cons x y) \Rightarrow (cons x y) ]
-
-\lambda x:False.
-  [\lambda h:False. True]
-  match x:False with []
-