From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 20 Feb 2006 13:59:46 +0000 (+0000)
Subject: Localization bug fixed.
X-Git-Tag: make_still_working~7550
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=54b20096e701de9f3fb8e10fe2106ab2f6e0d2bf;p=helm.git

Localization bug fixed.
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 37744982e..105631864 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -480,7 +480,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
               eat_prods true subst'' metasenv'' context 
-                he hetype tlbody_and_type ugraph2
+                he' hetype tlbody_and_type ugraph2
             in
               avoid_double_coercion context 
                 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
@@ -1159,7 +1159,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
         ~f:(fun _ ->
           (lazy ("The term " ^
             CicMetaSubst.ppterm_in_context subst he
-             context ^ "(that has type " ^
+             context ^ " (that has type " ^
             CicMetaSubst.ppterm_in_context subst hetype
              context ^ ") is here applied to " ^
             string_of_int (List.length tlbody_and_type) ^