X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=7b472a851b0e50839e0125a150e37163280875d1;hb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;hp=45b2bce8f79b97bdd29e02e795d37cd8e32a549c;hpb=b7aefa8f362d07bf9042f6879252345e69da07c8;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 45b2bce8f..7b472a851 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1192,11 +1192,6 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
          let selected =
            HExtlib.list_findopt
              (fun (metasenv,last,c) _ ->
-               match c with 
-               | c when not (CoercGraph.is_composite c) -> 
-                   debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
-                   None
-               | c ->
                let subst,metasenv,ugraph =
                 fo_unif_subst subst context metasenv last head ugraph in
                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));