diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-02 21:47:46 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-02 21:47:46 +0000 |
| commit | f7a91c9c1b323e2b15b3d7ae427ad0dd3dd8bf51 (patch) | |
| tree | 70b85be5fcb2dfd57ce38926d69623f9bf7c9792 /pretyping/cases.ml | |
| parent | 5e5d618bc8e642f0052dd5b99d5db97a452b8284 (diff) | |
Ajout de dynamiques pour les quotations constr et tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/cases.ml')
| -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 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) |