X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FlogicalOperations.ml;h=93c511f138336469b9bb5b3e9cc046effc9dd69f;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=5d06c95d21b55a94c72178eba18d9198771d68db;hpb=969d115cf2bc8d0fba05db54ab0886042f3d9512;p=helm.git diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index 5d06c95d2..93c511f13 100644 --- 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 _ -> []