X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftests%2Fmatch05.cic.test;h=1e80b5748a0a43a2295617babc0a919f8678e0c9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6bda244d487b4c16feb2dd06b0578a4e570a02cd;hpb=cab83f17a2d7a591c4ff2980b07946b50dbf9d00;p=helm.git

diff --git a/helm/gTopLevel/tests/match05.cic.test b/helm/gTopLevel/tests/match05.cic.test
index 6bda244d4..1e80b5748 100644
--- a/helm/gTopLevel/tests/match05.cic.test
+++ b/helm/gTopLevel/tests/match05.cic.test
@@ -2,6 +2,45 @@
 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#xpointer(1/1/2)
+alias id list = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1)
+alias id nil = cic:/CoRN/algebra/ListType/list.ind#xpointer(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#xpointer(1/1/2)
+alias id list = cic:/Coq/Lists/List/list.ind#xpointer(1/1)
+alias id nil = cic:/Coq/Lists/List/list.ind#xpointer(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#xpointer(1/1/2)
+alias id list = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1)
+alias id nil = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)
@@ -14,3 +53,20 @@ end
 ([x:list]list nil)
 ### (* REDUCED disambiguated term     *)
 nil
+###### INTERPRETATION NUMBER 4 ######
+### (* disambiguation environment  *)
+alias id cons = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1/2)
+alias id list = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1)
+alias id nil = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(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[_ ; _]}