From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 25 Oct 2005 13:46:52 +0000 (+0000)
Subject: "better" (????) identification of assertion failures
X-Git-Tag: V_0_7_2_3~195
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3813bdd5d0b4139a682b5faa50611791ac9278c2;p=helm.git

"better" (????) identification of assertion failures
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index a2a98bd0d..7c0d0e387 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -574,7 +574,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
           ) (subst'',metasenv'',ugraph2) pl1 pl2 
         with
          Invalid_argument _ ->
-          raise (UnificationFailure (lazy "6")))
+          raise (UnificationFailure (lazy "6.1")))
            (* (sprintf
               "Error trying to unify %s with %s: the number of branches is not the same." 
               (CicMetaSubst.ppterm subst t1) 
@@ -583,7 +583,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        if t1 = t2 then
          subst, metasenv,ugraph
        else
-        raise (UnificationFailure (lazy "6"))
+        raise (UnificationFailure (lazy "6.2"))
           (* (sprintf
              "Can't unify %s with %s because they are not convertible"
              (CicMetaSubst.ppterm subst t1)