added annotations to Cic.Implicit

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index f320f08379d78a5c33f94ca1ac807bd4f7e5e650..a9199c0e880f07b061a65d9b8655c334ec21eb6f 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -83,7 +83,7 @@ let metas_in_term term =
       C.Rel _ -> []
     | C.Meta (n,_) -> [n]
     | C.Sort _
-    | C.Implicit -> []
+    | C.Implicit _ -> []
     | C.Cast (te,ty) -> (aux te) @ (aux ty)
     | C.Prod (_,s,t) -> (aux s) @ (aux t)
     | C.Lambda (_,s,t) -> (aux s) @ (aux t)