diff options
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b5b246f213..fd6a0457d3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -315,7 +315,7 @@ let occur_rawconstr id = (array_exists occur tyl) or (not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv) | RCast (loc,c,t) -> (occur c) or (occur t) - | (RSort _ | RHole _ | RRef _ ) -> false + | (RSort _ | RHole _ | RRef _ | RMeta _) -> false and occur_pattern (idl,p,c) = not (List.mem id idl) & (occur c) |