diff options
| author | xclerc | 2013-09-19 12:59:04 +0000 |
|---|---|---|
| committer | xclerc | 2013-09-19 12:59:04 +0000 |
| commit | 826eb7c6d11007dfd747d49852e71a22e0a3850a (patch) | |
| tree | 25dce16a7107de4e0d3903e2808fb8f083d1f9ea /pretyping/patternops.ml | |
| parent | 33eea163c72c70eaa3bf76506c1d07a8cde911fd (diff) | |
Get rid of the uses of deprecated OCaml elements (still remaining compatible with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b804845993..e6a95a03e1 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -80,16 +80,16 @@ and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = let rec occur_meta_pattern = function | PApp (f,args) -> - (occur_meta_pattern f) or (Array.exists occur_meta_pattern args) - | PLambda (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) - | PProd (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) - | PLetIn (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) + (occur_meta_pattern f) || (Array.exists occur_meta_pattern args) + | PLambda (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) + | PProd (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) + | PLetIn (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) | PIf (c,c1,c2) -> - (occur_meta_pattern c) or - (occur_meta_pattern c1) or (occur_meta_pattern c2) + (occur_meta_pattern c) || + (occur_meta_pattern c1) || (occur_meta_pattern c2) | PCase(_,p,c,br) -> - (occur_meta_pattern p) or - (occur_meta_pattern c) or + (occur_meta_pattern p) || + (occur_meta_pattern c) || (List.exists (fun (_,_,p) -> occur_meta_pattern p) br) | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false |