X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=24242b42675f34f4f4cdefaca68cdaa1a2f4a5d4;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=49a68d1d0d23c9504f61c53248064d8410ee9c98;hpb=c982d8e516e990f19e9f5bdb4967a526095810f2;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 49a68d1d0..24242b426 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -192,7 +192,7 @@ let eta_fix metasenv t =
        in
        C.Meta (n,l')
    | C.Sort s -> C.Sort s
-   | C.Implicit -> C.Implicit
+   | C.Implicit _ as t -> t
    | C.Cast (v,t) -> C.Cast (eta_fix' context v, eta_fix' context t)
    | C.Prod (n,s,t) -> 
        C.Prod