From 9b0237f419714f67bfe4ae0cdee2c59986588e50 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 2 Mar 2004 17:12:19 +0000
Subject: [PATCH] - regtest now handles more than one interpretation: the tests
 committed   here have been ported to latest regtest format - more informative
 failure report

---
 helm/gTopLevel/regtest.ml              | 24 +++++++++--
 helm/gTopLevel/tests/fix00.cic.test    | 54 ++++++++++++++-----------
 helm/gTopLevel/tests/forall00.cic.test |  5 +++
 helm/gTopLevel/tests/lambda01.cic.test |  6 +++
 helm/gTopLevel/tests/lambda02.cic.test |  7 ++++
 helm/gTopLevel/tests/lambda03.cic.test |  7 ++++
 helm/gTopLevel/tests/match00.cic.test  |  7 ++++
 helm/gTopLevel/tests/match01.cic.test  |  8 ++++
 helm/gTopLevel/tests/match02.cic.test  |  8 ++++
 helm/gTopLevel/tests/match03.cic.test  |  7 ++++
 helm/gTopLevel/tests/match04.cic.test  |  5 +++
 helm/gTopLevel/tests/match05.cic.test  | 56 ++++++++++++++++++++++++++
 helm/gTopLevel/tests/match06.cic.test  |  4 ++
 helm/gTopLevel/tests/match07.cic.test  |  7 ++++
 14 files changed, 177 insertions(+), 28 deletions(-)

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index e31b1da05..4e72bdd54 100644
--- 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 901acd990..8719cbed3 100644
--- 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 1665098f7..29a06443b 100644
--- 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 8c9b561c4..4ca229fa8 100644
--- 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 fde5288f9..259140c9e 100644
--- 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 e6d731cde..4f21c8339 100644
--- 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 03db53319..b2de9dbd1 100644
--- 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 089665f6a..8d734e28f 100644
--- 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 c26510274..49f680053 100644
--- 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 16b4097e7..94681ed59 100644
--- 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 280bfbf5d..9c8016c60 100644
--- 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 6bda244d4..921264d6a 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:/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 d7078f0ac..041095638 100644
--- 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 ec1ad7156..a8331cff1 100644
--- 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      *)
-- 
2.39.2