- regtest now handles more than one interpretation: the tests committed

  here have been ported to latest regtest format
- more informative failure report

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index e31b1da05645605bef43461df06f5368d9772171..4e72bdd544616a50078e82e26910c2b2d84755e4 100644 (file)
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -191,17 +191,33 @@ let as_expected report_fname expected found =
  (if Sys.file_exists report_fname then Sys.remove report_fname) ;
  let och = lazy (open_out report_fname) in
  let print_endline s = print_endline_to_channel (Lazy.force och) s in
+  let print_interpretation test =
+    print_endline "## Interpretation dump ##";
+    print_endline "# Disambiguation environment:";
+    print_endline test.eenv;
+    print_endline "# Metasenv:";
+    print_endline test.emetasenv;
+    print_endline "# Term:";
+    print_endline test.eterm;
+    print_endline "# Type:";
+    print_endline test.etype;
+    print_endline "# Reduced term:";
+    print_endline test.ereduced;
+  in
   let rec aux =
    function
       [],[] -> true
     | ex::extl, fo::fotl ->
-       as_expected_one och ex fo &&
-       aux (extl,fotl)
+        let outcome1 = as_expected_one och ex fo in
+        let outcome2 = aux (extl,fotl) in
+        outcome1 && outcome2
     | [],found ->
-       print_endline "### Too many interpretations found" ;
+       print_endline "### Too many interpretations found:" ;
+       List.iter print_interpretation found;
        false
     | expected,[] ->
-       print_endline "### Too few interpretations found" ;
+       print_endline "### Too few interpretations found:" ;
+       List.iter print_interpretation expected;
        false
   in
    let outcome = aux (expected,found) in

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
index 901acd9904558f8fe78e3d7e03af94c5dca2b186..8719cbed32ebf6bbcbcb9cdb08422d3f06c70595 100644 (file)
--- a/helm/gTopLevel/tests/fix00.cic.test
+++ b/helm/gTopLevel/tests/fix00.cic.test
@@ -6,6 +6,12 @@ let rec fact =
     | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ]
 in
 (fact 4)
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
+alias id mult = cic:/Coq/Init/Peano/mult.con
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias num (instance 0) = "natural number"
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)
@@ -23,7 +29,7 @@ nat
 ### (* REDUCED disambiguated term     *)
 (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -31,7 +37,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -39,7 +45,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -47,7 +53,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -55,7 +61,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -63,7 +69,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -71,7 +77,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -79,7 +85,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -87,7 +93,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -95,7 +101,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -103,7 +109,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -111,7 +117,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -119,7 +125,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -127,7 +133,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -135,7 +141,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -143,7 +149,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -151,7 +157,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -159,7 +165,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -167,7 +173,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) O)))))) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -175,7 +181,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -183,7 +189,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -191,7 +197,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -199,7 +205,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  O O)) (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m
@@ -207,7 +213,7 @@ plus / 0 : (n:nat)(nat->nat) :=
 end}
  (S (
 Fix plus {
-plus / 0 : (n:nat)(nat->nat) := 
+plus / 0 : (n:nat)(m:nat)nat := 
 [n:nat][m:nat]
 <[n0:nat]nat>Cases n of 
  O => m

diff --git a/helm/gTopLevel/tests/forall00.cic.test b/helm/gTopLevel/tests/forall00.cic.test
index 1665098f72b96a166f82ba11821cc2a33b55ef6b..29a06443bd509a8c6ef6829579e03311d81a146b 100644 (file)
--- a/helm/gTopLevel/tests/forall00.cic.test
+++ b/helm/gTopLevel/tests/forall00.cic.test
@@ -1,4 +1,9 @@
 \forall n:nat. \forall m. n + m = n
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias symbol "eq" (instance 0) = "leibnitz's equality"
+alias symbol "plus" (instance 0) = "natural plus"
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/lambda01.cic.test b/helm/gTopLevel/tests/lambda01.cic.test
index 8c9b561c433f15f61df38055ecdf9039453d91fb..4ca229fa8dbd693901b906ee6d2cc5d68b8627b6 100644 (file)
--- a/helm/gTopLevel/tests/lambda01.cic.test
+++ b/helm/gTopLevel/tests/lambda01.cic.test
@@ -1,5 +1,11 @@
 (\lambda f. (f 0 (le_n 0))
   \lambda n. \lambda H. (refl_equal nat 0))
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#1/1/1
+alias num (instance 0) = "natural number"
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/lambda02.cic.test b/helm/gTopLevel/tests/lambda02.cic.test
index fde5288f91a4e5e35ad0eb899ee1809d8e8e5232..259140c9ef6253ce02211d430b6dce0f34a5c960 100644 (file)
--- a/helm/gTopLevel/tests/lambda02.cic.test
+++ b/helm/gTopLevel/tests/lambda02.cic.test
@@ -1,4 +1,11 @@
 \lambda f:(\forall n:nat. (\forall H:(le 0 n). (n=n))). (f 0 (le_n 0))
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id le = cic:/Coq/Init/Peano/le.ind#1/1
+alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias num (instance 0) = "natural number"
+alias symbol "eq" (instance 0) = "leibnitz's equality"
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/lambda03.cic.test b/helm/gTopLevel/tests/lambda03.cic.test
index e6d731cdec22c51ee60da30a507f3c6102d17559..4f21c833992db99fbb65e1daa29b6929ff75caaf 100644 (file)
--- a/helm/gTopLevel/tests/lambda03.cic.test
+++ b/helm/gTopLevel/tests/lambda03.cic.test
@@ -1,5 +1,12 @@
 \lambda n:nat.
  \lambda H:n=n.\lambda g:(?\to (le n 0))\to True.(g \lambda f.(f n H))
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id True = cic:/Coq/Init/Logic/True.ind#1/1
+alias id le = cic:/Coq/Init/Peano/le.ind#1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias num (instance 0) = "natural number"
+alias symbol "eq" (instance 0) = "leibnitz's equality"
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match00.cic.test b/helm/gTopLevel/tests/match00.cic.test
index 03db53319727fec61cfd5f9acff9c3a64c934166..b2de9dbd117d276058e23800302d00672257dc80 100644 (file)
--- a/helm/gTopLevel/tests/match00.cic.test
+++ b/helm/gTopLevel/tests/match00.cic.test
@@ -4,6 +4,13 @@
 match (S O):nat with
 [ O \Rightarrow O
 | (S x) \Rightarrow false ]
+###### 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 bool = cic:/Coq/Init/Datatypes/bool.ind#1/1
+alias id false = cic:/Coq/Init/Datatypes/bool.ind#1/1/2
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match01.cic.test b/helm/gTopLevel/tests/match01.cic.test
index 089665f6af4a89c0afe9bef6064c7e7813a5d036..8d734e28f271491a98bbb3d095f106690fa26fab 100644 (file)
--- a/helm/gTopLevel/tests/match01.cic.test
+++ b/helm/gTopLevel/tests/match01.cic.test
@@ -2,6 +2,14 @@
 match (le_n O): le with
 [ le_n \Rightarrow (refl_equal nat O)
 | (le_S x y) \Rightarrow (refl_equal nat O) ]
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
+alias id eq = cic:/Coq/Init/Logic/eq.ind#1/1
+alias id le = cic:/Coq/Init/Peano/le.ind#1/1
+alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#1/1/1
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match02.cic.test b/helm/gTopLevel/tests/match02.cic.test
index c265102742d4435892e0cf49f5d142a599589071..49f680053b51fe6ba23ab97226b4e7d0497d5485 100644 (file)
--- a/helm/gTopLevel/tests/match02.cic.test
+++ b/helm/gTopLevel/tests/match02.cic.test
@@ -2,6 +2,14 @@
 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)) ]
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
+alias id le = cic:/Coq/Init/Peano/le.ind#1/1
+alias id le_S = cic:/Coq/Init/Peano/le.ind#1/1/2
+alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias num (instance 0) = "natural number"
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match03.cic.test b/helm/gTopLevel/tests/match03.cic.test
index 16b4097e79a84d2c54f18556f1e660466845bf4e..94681ed5962b1910183d5d45e47ea7ccb67a6bab 100644 (file)
--- a/helm/gTopLevel/tests/match03.cic.test
+++ b/helm/gTopLevel/tests/match03.cic.test
@@ -2,6 +2,13 @@
 match true:bool with
 [ true \Rightarrow O
 | false \Rightarrow (S O) ]
+###### 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 bool = cic:/Coq/Init/Datatypes/bool.ind#1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id true = cic:/Coq/Init/Datatypes/bool.ind#1/1/1
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match04.cic.test b/helm/gTopLevel/tests/match04.cic.test
index 280bfbf5d26549be58b3c13f077c0aaed9788048..9c8016c60056c18b3460f5022f76c7188f135e5e 100644 (file)
--- a/helm/gTopLevel/tests/match04.cic.test
+++ b/helm/gTopLevel/tests/match04.cic.test
@@ -2,6 +2,11 @@
 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      *)

diff --git a/helm/gTopLevel/tests/match05.cic.test b/helm/gTopLevel/tests/match05.cic.test
index 6bda244d487b4c16feb2dd06b0578a4e570a02cd..921264d6ac04b1607d34d4c168a669e912107b0c 100644 (file)
--- 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:/Algebra/algebra/ListType/list.ind#1/1/2
+alias id list = cic:/Algebra/algebra/ListType/list.ind#1/1
+alias id nil = cic:/Algebra/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      *)
@@ -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#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[_ ; _]}

diff --git a/helm/gTopLevel/tests/match06.cic.test b/helm/gTopLevel/tests/match06.cic.test
index d7078f0ac0a77d0bedf3ec1098fbfe0fe8ead918..0410956381d04f3099214fe854687e9ae4e57d7b 100644 (file)
--- a/helm/gTopLevel/tests/match06.cic.test
+++ b/helm/gTopLevel/tests/match06.cic.test
@@ -1,6 +1,10 @@
 \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#1/1
+alias id True = cic:/Coq/Init/Logic/True.ind#1/1
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)

diff --git a/helm/gTopLevel/tests/match07.cic.test b/helm/gTopLevel/tests/match07.cic.test
index ec1ad7156708bebcfa6aad5c98659f50a9048f01..a8331cff18379052a38e980065322012ef3d5617 100644 (file)
--- a/helm/gTopLevel/tests/match07.cic.test
+++ b/helm/gTopLevel/tests/match07.cic.test
@@ -2,6 +2,13 @@
 match true with
 [ true \Rightarrow O
 | false \Rightarrow (S O) ]
+###### 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 bool = cic:/Coq/Init/Datatypes/bool.ind#1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id true = cic:/Coq/Init/Datatypes/bool.ind#1/1/1
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)