Check missed: the two metasenv were not compared.

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index 2530e34a0ebf1387c99bf10e68f0333f69dfb423..8f42a29fcfbcaa23343fb78f0c9b55f044d5c376 100644 (file)
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -108,6 +108,14 @@ let parse_regtest =
 
 let as_expected expected found = (* ignores "term" field *)
   let outcome = ref true in
+  if expected.emetasenv <> found.emetasenv then begin
+    print_msg "Metasenv mismatch";
+    print_msg "  expected:";
+    print_msg ("  " ^ expected.emetasenv);
+    print_msg "  found:";
+    print_msg ("  " ^ found.emetasenv);
+    outcome := false;
+  end;
   if expected.eterm <> found.eterm then begin
     print_msg "Term mismatch";
     print_msg "  expected:";