X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2Facic2content.ml;h=69a1f632dcf3117138c5b421dcfb94f9999adb10;hb=3e198ec27dc8f3a29cb2a64c7e0354006aa86352;hp=ddd1b5ebcd02687a6d9a8834497fc9ebc984bf70;hpb=af01cbe989c6d633cb79f4efc0d2d0fee1eeb8cc;p=helm.git

diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml
index ddd1b5ebc..69a1f632d 100644
--- a/components/acic_content/acic2content.ml
+++ b/components/acic_content/acic2content.ml
@@ -360,7 +360,7 @@ let infer_dependent ~headless context metasenv = function
                   (n <> Cic.Anonymous && fstorder src, t) :: 
                   aux (CicSubstitution.subst 
                         (Deannotate.deannotate_term t) tgt) tl
-              | _ -> assert false
+              | _ -> List.map (fun s -> false,s) (t::tl)
        in
        (false, he) :: aux hety tl
      with CicTypeChecker.TypeCheckerFailure _ -> assert false