X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=3c8b077297fd5ad8da82700f4dd081fade124c19;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=1dc4ae2bd0f08c373e7b96d359fa7a4a9e8ac249;hpb=44f465fa4b07556033c5c6c196a52cf16599589c;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 1dc4ae2bd..3c8b07729 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -144,7 +144,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive constructors"
         (CicPp.ppterm t1) (CicPp.ppterm t1)))
-   | (C.Implicit, _) | (_, C.Implicit) ->  assert false
+   | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
    | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->