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

6 files changed, 15 insertions, 15 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 96bbf07d5..475bc098a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -120,7 +120,7 @@ let open_constant i ((sp,kn), obj) =
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let exists_name id =
-  variable_exists id or Global.exists_objlabel (Label.of_id id)
+  variable_exists id || Global.exists_objlabel (Label.of_id id)
 
 let check_exists sp =
   let id = basename sp in
diff --git a/library/goptions.ml b/library/goptions.ml
index 4151e6774..6e2c6ae72 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -211,7 +211,7 @@ let check_key key = try
   error "Sorry, this option name is already used."
 with Not_found ->
   if List.mem_assoc (nickname key) !string_table
-    or List.mem_assoc (nickname key) !ref_table
+    || List.mem_assoc (nickname key) !ref_table
   then error "Sorry, this option name is already used."
 
 open Libobject
diff --git a/library/heads.ml b/library/heads.ml
index 2a42888d5..c52a5eb23 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -109,7 +109,7 @@ let kind_of_head env t =
           (* enough arguments to [cst] *)
           k,List.skipn n l,List.nth l (i-1) in
       let l' = List.make q (mkMeta 0) @ rest in
-      aux k' l' a (with_subcase or with_case)
+      aux k' l' a (with_subcase || with_case)
   | ConstructorHead when with_case -> NotImmediatelyComputableHead
   | x -> x
   in aux 0 [] t false
diff --git a/library/impargs.ml b/library/impargs.ml
index 0026bc489..66900ee42 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -174,8 +174,8 @@ let is_flexible_reference env bound depth f =
 let push_lift d (e,n) = (push_rel d e,n+1)
 
 let is_reversible_pattern bound depth f l =
-  isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) &
-  Array.for_all (fun c -> isRel c & destRel c < depth) l &
+  isRel f && let n = destRel f in (n < bound+depth) && (n >= depth) &&
+  Array.for_all (fun c -> isRel c && destRel c < depth) l &&
   Array.distinct l
 
 (* Precondition: rels in env are for inductive types only *)
@@ -184,13 +184,13 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
     let hd = if strict then whd_betadeltaiota env c else c in
     let c = if strongly_strict then hd else c in
     match kind_of_term hd with
-    | Rel n when (n < bound+depth) & (n >= depth) ->
+    | Rel n when (n < bound+depth) && (n >= depth) ->
 	let i = bound + depth - n - 1 in
         acc.(i) <- update pos rig acc.(i)
-    | App (f,l) when revpat & is_reversible_pattern bound depth f l ->
+    | App (f,l) when revpat && is_reversible_pattern bound depth f l ->
 	let i = bound + depth - destRel f - 1 in
 	acc.(i) <- update pos rig acc.(i)
-    | App (f,_) when rig & is_flexible_reference env bound depth f ->
+    | App (f,_) when rig && is_flexible_reference env bound depth f ->
 	if strict then () else
           iter_constr_with_full_binders push_lift (frec false) ed c
     | Case _ when rig ->
@@ -246,7 +246,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
 
 let compute_implicits_flags env f all t =
   compute_implicits_gen
-    (f.strict or f.strongly_strict) f.strongly_strict
+    (f.strict || f.strongly_strict) f.strongly_strict
     f.reversible_pattern f.contextual all env t
 
 let compute_auto_implicits env flags enriching t =
@@ -289,9 +289,9 @@ let force_inference_of = function
 (* [in_ctx] means we know the expected type, [n] is the index of the argument *)
 let is_inferable_implicit in_ctx n = function
   | None -> false
-  | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p
+  | Some (_,DepRigid (Hyp p),_) -> in_ctx || n >= p
   | Some (_,DepFlex (Hyp p),_) -> false
-  | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q
+  | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx || n >= q
   | Some (_,DepRigid Conclusion,_) -> in_ctx
   | Some (_,DepFlex Conclusion,_) -> false
   | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
@@ -328,7 +328,7 @@ let check_correct_manual_implicits autoimps l =
 	if not forced then
 	  error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".")
     | ExplByPos (i,_id),_t ->
-	if i<1 or i>List.length autoimps then
+	if i<1 || i>List.length autoimps then
 	  error ("Bad implicit argument number: "^(string_of_int i)^".")
 	else
 	  errorlabstrm ""
@@ -663,7 +663,7 @@ let declare_manual_implicits local ref ?enriching l =
     | _ ->
 	check_rigidity isrigid;
 	let l = List.map (fun imps -> (imps,List.length imps)) l in
-	let l = Sort.list (fun (_,n1) (_,n2) -> n1 > n2) l in
+	let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
 	check_inclusion l;
 	let nargs = List.length autoimpls in
 	List.map (fun (imps,n) ->
diff --git a/library/library.ml b/library/library.ml
index 44e8286ce..2a495f0cf 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -144,7 +144,7 @@ let open_library export explicit_libs m =
     (* Only libraries indirectly to open are not reopen *)
     (* Libraries explicitly mentionned by the user are always reopen *)
     List.exists (eq_lib_name m) explicit_libs
-    or not (library_is_opened m.library_name)
+    || not (library_is_opened m.library_name)
   then begin
     register_open_library export m;
     Declaremods.really_import_module (MPfile m.library_name)
diff --git a/library/nameops.ml b/library/nameops.ml
index 22a21a4d5..a62d55dfc 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -58,7 +58,7 @@ let make_ident sa = function
   | Some n ->
       let c = Char.code (String.get sa (String.length sa -1)) in
       let s =
-        if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
+        if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n)
         else sa ^ "_" ^ (string_of_int n) in
       Id.of_string s
   | None -> Id.of_string (String.copy sa)