From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Feb 2004 14:49:16 +0000 (+0000)
Subject: Check missed: the two metasenv were not compared.
X-Git-Tag: V_0_2_3~88
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=54bd214a34224eab8c5ef2a26cb832c8b1ff122f;p=helm.git

Check missed: the two metasenv were not compared.
---

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index 2530e34a0..8f42a29fc 100644
--- 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:";