diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-02 17:16:33 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-02 17:16:33 +0000 |
| commit | 7d243d68abf11feeb7a6c421fb75505205938a80 (patch) | |
| tree | 1891eb5fc10d959f9d34acab0c7c800cb73f1994 /pretyping | |
| parent | 7003ff317ba1fce8898538801a1c8ecf1fddb972 (diff) | |
pattern-matching non-exhaustif (occur_rawconstr)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@398 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -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 b5b246f21..fd6a0457d 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) |