added annotations to Cic.Implicit

[helm.git] / helm / ocaml / cic_omdoc / eta_fixing.ml

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 49a68d1d0d23c9504f61c53248064d8410ee9c98..24242b42675f34f4f4cdefaca68cdaa1a2f4a5d4 100644 (file)
--- 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