]> matita.cs.unibo.it Git - helm.git/commitdiff
Localization bug fixed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 20 Feb 2006 13:59:46 +0000 (13:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 20 Feb 2006 13:59:46 +0000 (13:59 +0000)
helm/software/components/cic_unification/cicRefine.ml

index 37744982e5689e4f6a7c005660fdc8a080b09538..10563186461a2601c30d4799d7c6657db8231da0 100644 (file)
@@ -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) ^