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

8 files changed, 31 insertions, 31 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d743135a24..6ed05d6b35 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -148,7 +148,7 @@ let rebuild_dn st ((l,l',dn) : search_entry) =
 let lookup_tacs (hdc,c) st (l,l',dn) =
   let l'  = List.map snd (Bounded_net.lookup st dn c) in
   let sl' = List.stable_sort pri_order_int l' in
-    Sort.merge pri_order l sl'
+    List.merge pri_order_int l sl'
 
 module Constr_map = Map.Make(RefOrdered)
 
@@ -334,16 +334,16 @@ module Hint_db = struct
     with Not_found -> empty_se
  
   let map_none db =
-    List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) [])
+    List.map snd (List.merge pri_order_int (List.map snd db.hintdb_nopat) [])
     
   let map_all k db =
     let (l,l',_) = find k db in
-      List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
+      List.map snd (List.merge pri_order_int (List.map snd db.hintdb_nopat @ l) l')
 
   let map_auto (k,c) db =
     let st = if db.use_dn then Some db.hintdb_state else None in
     let l' = lookup_tacs (k,c) st (find k db) in
-      List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
+      List.map snd (List.merge pri_order_int (List.map snd db.hintdb_nopat) l')
 
   let is_exact = function
     | Give_exact _ -> true
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 14a9ae9c2d..d6e51a15d6 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -65,7 +65,7 @@ let contradiction_context gl =
 
 let is_negation_of env sigma typ t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
-    | Prod (na,t,u) -> is_empty_type u & is_conv_leq env sigma typ t
+    | Prod (na,t,u) -> is_empty_type u && is_conv_leq env sigma typ t
     | _ -> false
 
 let contradiction_term (c,lbind as cl) gl =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 49b7ec710d..1756f89ceb 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -32,7 +32,7 @@ open Locusops
 let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
 
 let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
-  if occur_existential t1 or occur_existential t2 then
+  if occur_existential t1 || occur_existential t2 then
      tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl
   else exact_check c gl
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d1d4e003d6..04d6b9d8e8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -480,7 +480,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
   in
   let t1 = pf_apply get_type_of gl c1
   and t2 = pf_apply get_type_of gl c2 in
-  if unsafe or (pf_conv_x gl t1 t2) then
+  if unsafe || (pf_conv_x gl t1 t2) then
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
     let eq = applist (e, [t1;c1;c2]) in
@@ -1060,7 +1060,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 let make_iterated_tuple env sigma dflt (z,zty) =
   let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
   let sort_of_zty = get_sort_of env sigma zty in
-  let sorted_rels = Sort.list (<) (Int.Set.elements rels) in
+  let sorted_rels = List.sort Pervasives.compare (Int.Set.elements rels) in
   let (tuple,tuplety) =
     List.fold_left (make_tuple env sigma) (z,zty) sorted_rels
   in
@@ -1208,7 +1208,7 @@ let postInjEqTac ipats c n =
 
 let injEq ipats =
   let l2r =
-    if use_injection_pattern_l2r_order () & ipats <> None then true else false
+    if use_injection_pattern_l2r_order () && ipats <> None then true else false
   in
   injEqThen (postInjEqTac ipats) l2r
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index d870bfa1d8..534b90491a 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -91,7 +91,7 @@ let match_with_one_constructor style onlybinary allow_rec t =
   | Ind ind ->
       let (mib,mip) = Global.lookup_inductive ind in
       if Int.equal (Array.length mip.mind_consnames) 1
-	&& (allow_rec or not (mis_is_recursive (ind,mib,mip)))
+	&& (allow_rec || not (mis_is_recursive (ind,mib,mip)))
         && (Int.equal mip.mind_nrealargs 0)
       then
 	if is_strict_conjunction style (* strict conjunction *) then
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ed22ab0e18..ec96a887dc 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -49,7 +49,7 @@ let check_no_metas clenv ccl =
 
 let var_occurs_in_pf gl id =
   let env = pf_env gl in
-  occur_var env id (pf_concl gl) or
+  occur_var env id (pf_concl gl) ||
   List.exists (occur_var_in_decl env id) (pf_hyps gl)
 
 (* [make_inv_predicate (ity,args) C]
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index b397bcaa3f..f0a7577326 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -195,7 +195,7 @@ let intern_ltac_variable ist = function
       raise Not_found
 
 let intern_constr_reference strict ist = function
-  | Ident (_,id) as r when not strict & find_hyp id ist ->
+  | Ident (_,id) as r when not strict && find_hyp id ist ->
       GVar (dloc,id), Some (CRef r)
   | Ident (_,id) as r when find_ctxvar id ist ->
       GVar (dloc,id), if strict then None else Some (CRef r)
@@ -361,7 +361,7 @@ let intern_evaluable_reference_or_by_notation ist = function
 (* Globalize a reduction expression *)
 let intern_evaluable ist = function
   | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
-  | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist ->
+  | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist ->
       ArgArg (EvalVarRef id, Some (loc,id))
   | AN (Ident (loc,id)) when find_ctxvar id ist ->
       ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e97b01d388..4a60f6559a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -452,9 +452,9 @@ let build_intro_tac id dest tac = match dest with
 
 let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl =
   match kind_of_term (pf_concl gl) with
-    | Prod (name,t,u) when not dep_flag or (dependent (mkRel 1) u) ->
+    | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
 	build_intro_tac (find_name loc (name,None,t) gl name_flag) move_flag tac gl
-    | LetIn (name,b,t,u) when not dep_flag or (dependent (mkRel 1) u) ->
+    | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
 	build_intro_tac (find_name loc (name,Some b,t) gl name_flag) move_flag tac
 	  gl
     | _ ->
@@ -736,7 +736,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c
     else clenv
   in
   let new_hyp_typ = clenv_type clenv in
-  if not with_evars & occur_meta new_hyp_typ then
+  if not with_evars && occur_meta new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
   tclTHEN
@@ -1142,8 +1142,8 @@ let (assumption : tactic) = fun gl ->
     | [] ->
         if only_eq then arec false hyps else error "No such assumption."
     | (id,c,t)::rest ->
-	if (only_eq & eq_constr t concl)
-          or (not only_eq & pf_conv_x_leq gl t concl)
+	if (only_eq && eq_constr t concl)
+          || (not only_eq && pf_conv_x_leq gl t concl)
         then refine_no_check (mkVar id) gl
 	else arec only_eq rest
   in
@@ -1231,8 +1231,8 @@ let keep hyps gl =
   let cl,_ =
     fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
       if List.mem hyp hyps
-	or List.exists (occur_var_in_decl env hyp) keep
-	or occur_var env hyp ccl
+        || List.exists (occur_var_in_decl env hyp) keep
+	|| occur_var env hyp ccl
       then (clear,decl::keep)
       else (hyp::clear,keep))
       ~init:([],[]) (pf_env gl)
@@ -1369,9 +1369,9 @@ let rewrite_hyp l2r id gl =
   (* TODO: detect setoid equality? better detect the different equalities *)
   match match_with_equality_type t with
   | Some (hdcncl,[_;lhs;rhs]) ->
-      if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then
+      if l2r && isVar lhs && not (occur_var (pf_env gl) (destVar lhs) rhs) then
 	subst_on l2r (destVar lhs) rhs gl
-      else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then
+      else if not l2r && isVar rhs && not (occur_var (pf_env gl) (destVar rhs) lhs) then
 	subst_on l2r (destVar rhs) lhs gl
       else
 	tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
@@ -1602,7 +1602,7 @@ let generalize_dep ?(with_let=false) c gl =
   let init_ids = ids_of_named_context (Global.named_context()) in
   let seek d toquant =
     if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant
-      or dependent_in_decl c d then
+      || dependent_in_decl c d then
       d::toquant
     else
       toquant in
@@ -1612,7 +1612,7 @@ let generalize_dep ?(with_let=false) c gl =
   let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
   let tothin' =
     match kind_of_term c with
-      | Var id when mem_named_context id sign & not (List.mem id init_ids)
+      | Var id when mem_named_context id sign && not (List.mem id init_ids)
 	  -> id::tothin
       | _ -> tothin
   in
@@ -2330,7 +2330,7 @@ let make_up_names n ind_opt cname =
     else add_prefix ind_prefix cname in
   let hyprecname = make_base n base_ind in
   let avoid =
-    if Int.equal n 1 (* Only one recursive argument *) or Int.equal n 0 then []
+    if Int.equal n 1 (* Only one recursive argument *) || Int.equal n 0 then []
     else
       (* Forbid to use cname, cname0, hyprecname and hyprecname0 *)
       (* in order to get names such as f1, f2, ... *)
@@ -2787,7 +2787,7 @@ let compute_elim_sig ?elimc elimt =
 	    let hi_args_enough = (* hi a le bon nbre d'arguments *)
 	      Int.equal (List.length hi_args) (List.length params + !res.nargs -1) in
 	    (* FIXME: Ces deux tests ne sont pas suffisants. *)
-	    if not (hi_is_ind & hi_args_enough) then raise Exit (* No indarg *)
+	    if not (hi_is_ind && hi_args_enough) then raise Exit (* No indarg *)
 	    else (* Last arg is the indarg *)
 	      res := {!res with
 		indarg = Some (List.hd !res.args);
@@ -2826,14 +2826,14 @@ let compute_scheme_signature scheme names_info ind_type_guess =
 	      List.equal eq_constr
 		(List.lastn scheme.nargs indargs)
 		(extended_rel_list 0 scheme.args) in
-	    if not (ccl_arg_ok & ind_is_ok) then
+	    if not (ccl_arg_ok && ind_is_ok) then
 	      error_ind_scheme "the conclusion of"
 	  in (cond, check_concl)
   in
   let is_pred n c =
     let hd = fst (decompose_app c) in
     match kind_of_term hd with
-      | Rel q when n < q & q <= n+scheme.npredicates -> IndArg
+      | Rel q when n < q && q <= n+scheme.npredicates -> IndArg
       | _ when cond hd -> RecArg
       | _ -> OtherArg
   in
@@ -3209,7 +3209,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl =
       | c::l' ->
 	  match kind_of_term c with
 	    | Var id when not (mem_named_context id (Global.named_context()))
-		& not with_evars ->
+		&& not with_evars ->
 		let _ = newlc:= id::!newlc in
 		atomize_list l' gl
 
@@ -3567,7 +3567,7 @@ let intros_transitivity  n  = tclTHEN intros (transitivity_gen n)
 
 let interpretable_as_section_decl d1 d2 = match d1,d2 with
   | (_,Some _,_), (_,None,_) -> false
-  | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2
+  | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 && eq_constr t1 t2
   | (_,None,t1), (_,_,t2) -> eq_constr t1 t2
 
 let abstract_subproof id tac gl =
@@ -3576,7 +3576,7 @@ let abstract_subproof id tac gl =
   let sign,secsign =
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) ->
-	if mem_named_context id current_sign &
+	if mem_named_context id current_sign &&
           interpretable_as_section_decl (Context.lookup_named id current_sign) d
         then (s1,push_named_context_val d s2)
 	else (add_named_decl d s1,s2))