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

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

diff --git a/helm/gTopLevel/tests/match05.cic.test b/helm/gTopLevel/tests/match05.cic.test
deleted file mode 100644 (file)
index 0c77d5d..0000000
--- a/helm/gTopLevel/tests/match05.cic.test
+++ /dev/null
@@ -1,72 +0,0 @@
-[\lambda x:list. list]
-match nil:list with
-[ nil \Rightarrow nil
-| (cons x y) \Rightarrow (cons x y) ]
-###### INTERPRETATION NUMBER 1 ######
-### (* disambiguation environment  *)
-alias id cons = cic:/CoRN/algebra/ListType/list.ind#1/1/2
-alias id list = cic:/CoRN/algebra/ListType/list.ind#1/1
-alias id nil = cic:/CoRN/algebra/ListType/list.ind#1/1/1
-### (* METASENV after disambiguation  *)
-_ :? _; _ :? _ |- ?25: Type
-### (* TERM after disambiguation      *)
-
-<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of 
- nil => nil{A:=?25[_ ; _]}
- cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
-end
-### (* TYPE_OF the disambiguated term *)
-([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
-### (* REDUCED disambiguated term     *)
-nil{A:=?25[_ ; _]}
-###### INTERPRETATION NUMBER 2 ######
-### (* disambiguation environment  *)
-alias id cons = cic:/Coq/Lists/List/list.ind#1/1/2
-alias id list = cic:/Coq/Lists/List/list.ind#1/1
-alias id nil = cic:/Coq/Lists/List/list.ind#1/1/1
-### (* METASENV after disambiguation  *)
-_ :? _; _ :? _ |- ?25: Set
-### (* TERM after disambiguation      *)
-
-<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of 
- nil => nil{A:=?25[_ ; _]}
- cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
-end
-### (* TYPE_OF the disambiguated term *)
-([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
-### (* REDUCED disambiguated term     *)
-nil{A:=?25[_ ; _]}
-###### INTERPRETATION NUMBER 3 ######
-### (* disambiguation environment  *)
-alias id cons = cic:/Coq/Lists/MonoList/list.ind#1/1/2
-alias id list = cic:/Coq/Lists/MonoList/list.ind#1/1
-alias id nil = cic:/Coq/Lists/MonoList/list.ind#1/1/1
-### (* METASENV after disambiguation  *)
-
-### (* TERM after disambiguation      *)
-
-<[x:list]list>Cases nil of 
- nil => nil
- cons => [x:A][y:list](cons x y)
-end
-### (* TYPE_OF the disambiguated term *)
-([x:list]list nil)
-### (* REDUCED disambiguated term     *)
-nil
-###### INTERPRETATION NUMBER 4 ######
-### (* disambiguation environment  *)
-alias id cons = cic:/Lannion/continuations/weight/specif/list.ind#1/1/2
-alias id list = cic:/Lannion/continuations/weight/specif/list.ind#1/1
-alias id nil = cic:/Lannion/continuations/weight/specif/list.ind#1/1/1
-### (* METASENV after disambiguation  *)
-_ :? _; _ :? _ |- ?25: Set
-### (* TERM after disambiguation      *)
-
-<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of 
- nil => nil{A:=?25[_ ; _]}
- cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
-end
-### (* TYPE_OF the disambiguated term *)
-([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
-### (* REDUCED disambiguated term     *)
-nil{A:=?25[_ ; _]}