now destruct takes an optional list of term rather than a sigle optional term

[helm.git] / components / cic_unification / cicRefine.ml

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 4b310ef75637fd6a1e1127fcbc181a84fa4006fd..e0f8fd1c79128ad1663640690a167c931ce623cb 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -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