added annotations to Cic.Implicit

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

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 5d06c95d21b55a94c72178eba18d9198771d68db..93c511f138336469b9bb5b3e9cc046effc9dd69f 100644 (file)
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -42,7 +42,7 @@ let get_context ids_to_terms ids_to_father_ids =
          | C.Var _
          | C.Meta _
          | C.Sort _
-         | C.Implicit
+         | C.Implicit _
          | C.Cast _ -> []
          | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
          | C.Prod _ -> []