aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6f051b6e3..2535c2b34 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -534,7 +534,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 _ | REvar _ | RMeta _) -> false
+ | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _ | RDynamic _) -> false
and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)