From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 27 Sep 2006 15:04:14 +0000 (+0000)
Subject: More informative error message.
X-Git-Tag: 0.4.95@7852~986
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=020ec6bc6c14c1e39b2564da314a6079bb34f79c;p=helm.git

More informative error message.
---

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index ecde4cdfd..6004e73fa 100644
--- a/components/cic_unification/cicUnification.ml
+++ b/components/cic_unification/cicUnification.ml
@@ -457,18 +457,19 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
           (sprintf
             "Can't unify %s with %s due to different constants"
             (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2)))) 
+            (CicMetaSubst.ppterm subst t2))))
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
        if UriManager.eq uri1 uri2 && i1 = i2 then
          fo_unif_subst_exp_named_subst 
            test_equality_only 
            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
        else
-         raise (UnificationFailure (lazy "4"))
-           (* (sprintf
-              "Can't unify %s with %s due to different inductive principles"
-              (CicMetaSubst.ppterm subst t1) 
-              (CicMetaSubst.ppterm subst t2))) *)
+         raise (UnificationFailure
+           (lazy
+            (sprintf
+             "Can't unify %s with %s due to different inductive principles"
+             (CicMetaSubst.ppterm subst t1) 
+             (CicMetaSubst.ppterm subst t2))))
    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
@@ -476,11 +477,12 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
            test_equality_only 
            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
        else
-         raise (UnificationFailure (lazy "5"))
-           (* (sprintf
+         raise (UnificationFailure
+          (lazy
+            (sprintf
               "Can't unify %s with %s due to different inductive constructors"
               (CicMetaSubst.ppterm subst t1) 
-              (CicMetaSubst.ppterm subst t2))) *)
+              (CicMetaSubst.ppterm subst t2))))
    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
                               subst context metasenv te t2 ugraph