Localization bug fixed.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 37744982e5689e4f6a7c005660fdc8a080b09538..10563186461a2601c30d4799d7c6657db8231da0 100644 (file)
--- 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) ^