diff options
| author |  xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 12:59:04 +0000 |
|---|---|---|
| committer | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 12:59:04 +0000 |
| commit | 826eb7c6d11007dfd747d49852e71a22e0a3850a (patch) | |
| tree | 25dce16a7107de4e0d3903e2808fb8f083d1f9ea /pretyping/glob_ops.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/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index e219bbeb1..88702b350 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -126,7 +126,7 @@ let same_id na id = match na with let occur_glob_constr id = let rec occur = function | GVar (loc,id') -> Id.equal id id' - | GApp (loc,f,args) -> (occur f) or (List.exists occur args) + | GApp (loc,f,args) -> (occur f) || (List.exists occur args) | GLambda (loc,na,bk,ty,c) -> (occur ty) || (not (same_id na id) && (occur c)) | GProd (loc,na,bk,ty,c) -> @@ -135,13 +135,13 @@ let occur_glob_constr id = (occur b) || (not (same_id na id) && (occur c)) | GCases (loc,sty,rtntypopt,tml,pl) -> (occur_option rtntypopt) - or (List.exists (fun (tm,_) -> occur tm) tml) - or (List.exists occur_pattern pl) + || (List.exists (fun (tm,_) -> occur tm) tml) + || (List.exists occur_pattern pl) | GLetTuple (loc,nal,rtntyp,b,c) -> occur_return_type rtntyp id - or (occur b) or (not (List.mem (Name id) nal) & (occur c)) + || (occur b) || (not (List.mem (Name id) nal) && (occur c)) | GIf (loc,c,rtntyp,b1,b2) -> - occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2) + occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2) | GRec (loc,fk,idl,bl,tyl,bv) -> not (Array.for_all4 (fun fid bl ty bd -> let rec occur_fix = function @@ -154,11 +154,11 @@ let occur_glob_constr id = (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | GCast (loc,c,k) -> (occur c) or (match k with CastConv t + | GCast (loc,c,k) -> (occur c) || (match k with CastConv t | CastVM t | CastNative t -> occur t | CastCoerce -> false) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false - and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) + and occur_pattern (loc,idl,p,c) = not (List.mem id idl) && (occur c) and occur_option = function None -> false | Some p -> occur p |