X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=e4f4ef8e0c002a600f791d37ec2f9524730dbefb;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=4b310ef75637fd6a1e1127fcbc181a84fa4006fd;hpb=14d7d5934b20810a2479630c55c59557aba83a7f;p=helm.git

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 4b310ef75..e4f4ef8e0 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -91,7 +91,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn =
   try
    Cic.CicHash.find localization_tbl t
   with Not_found ->
-   prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
+   HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
    raise exn'
  in
   raise (HExtlib.Localized (loc,exn'))
@@ -527,6 +527,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        (lazy ("Unkown mutual inductive definition " ^ 
                          U.string_of_uri uri)))
            in
+           if List.length constructors <> List.length pl then
+            enrich localization_tbl t
+             (RefineFailure
+               (lazy "Wrong number of cases")) ;
            let rec count_prod t =
              match CicReduction.whd ~subst context t with
                  C.Prod (_, _, t) -> 1 + (count_prod t)
@@ -957,7 +961,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                | Some t,Some (_,C.Def (ct,_)) ->
                    let subst',metasenv',ugraph' = 
                    (try
-prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
+(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
+ * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
                       fo_unif_subst subst context metasenv t ct ugraph
                     with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
                    in
@@ -1329,7 +1334,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
                 " <==> " ^
-                CicMetaSubst.ppterm_in_context ~metasenv subst t context));
+                CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
+                "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
+                context));
                 debug_print (lazy ("FO_UNIF_SUBST: " ^
                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
                 let subst,metasenv,ugraph =