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

5 files changed, 27 insertions, 27 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7ba8617048..741ef9853a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -282,7 +282,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
     | _ ->
   try
-    if !Flags.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print || !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
     match availability_of_prim_token p sc scopes with
       | None -> raise No_match
@@ -291,7 +291,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
   with No_match ->
     try
-      if !Flags.raw_print or !print_no_symbol then raise No_match;
+      if !Flags.raw_print || !print_no_symbol then raise No_match;
       extern_symbol_pattern scopes vars pat
 	(uninterp_cases_pattern_notations pat)
     with No_match ->
@@ -409,7 +409,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
     CPatCstr (Loc.ghost, c, add_patt_for_params ind args, [])
   else
     try
-      if !Flags.raw_print or !print_no_symbol then raise No_match;
+      if !Flags.raw_print || !print_no_symbol then raise No_match;
       let (sc,p) = uninterp_prim_token_ind_pattern ind args in
       match availability_of_prim_token p sc scopes with
 	| None -> raise No_match
@@ -417,7 +417,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
 	  insert_pat_delimiters Loc.ghost (CPatPrim(Loc.ghost,p)) key
     with No_match ->
       try
-	if !Flags.raw_print or !print_no_symbol then raise No_match;
+	if !Flags.raw_print || !print_no_symbol then raise No_match;
 	extern_symbol_ind_pattern scopes vars ind args
 	  (uninterp_ind_pattern_notations ind)
     with No_match ->
@@ -439,7 +439,7 @@ let occur_name na aty =
     | Anonymous -> false
 
 let is_projection nargs = function
-  | Some r when not !Flags.raw_print & !print_projections ->
+  | Some r when not !Flags.raw_print && !print_projections ->
       (try
 	let n = Recordops.find_projection_nparams r + 1 in
 	if n <= nargs then Some n else None
@@ -463,11 +463,11 @@ let explicitize loc inctx impl (cf,f) args =
     | a::args, imp::impl when is_status_implicit imp ->
         let tail = exprec (q+1) (args,impl) in
         let visible =
-          !Flags.raw_print or
-          (!print_implicits & !print_implicits_explicit_args) or
-          (is_needed_for_correct_partial_application tail imp) or
-	  (!print_implicits_defensive &
-	   is_significant_implicit a &
+          !Flags.raw_print ||
+          (!print_implicits && !print_implicits_explicit_args) ||
+          (is_needed_for_correct_partial_application tail imp) ||
+	  (!print_implicits_defensive &&
+	   is_significant_implicit a &&
 	   not (is_inferable_implicit inctx n imp))
 	in
         if visible then
@@ -506,7 +506,7 @@ let extern_app loc inctx impl (cf,f) args =
     CAppExpl (loc, (None, f), [])
   else if not !Constrintern.parsing_explicit &&
     ((!Flags.raw_print ||
-      (!print_implicits & not !print_implicits_explicit_args)) &
+      (!print_implicits && not !print_implicits_explicit_args)) &&
      List.exists is_status_implicit impl)
   then
     CAppExpl (loc, (is_projection (List.length args) cf, f), args)
@@ -524,11 +524,11 @@ let rec extern_args extern scopes env args subscopes =
 
 let rec remove_coercions inctx = function
   | GApp (loc,GRef (_,r),args) as c
-      when  not (!Flags.raw_print or !print_coercions)
+      when  not (!Flags.raw_print || !print_coercions)
       ->
       let nargs = List.length args in
       (try match Classops.hide_coercion r with
-	  | Some n when n < nargs && (inctx or n+1 < nargs) ->
+	  | Some n when n < nargs && (inctx || n+1 < nargs) ->
 	      (* We skip a coercion *)
 	      let l = List.skipn n args in
 	      let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
@@ -583,12 +583,12 @@ let extern_glob_sort = function
 let rec extern inctx scopes vars r =
   let r' = remove_coercions inctx r in
   try
-    if !Flags.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print || !print_no_symbol then raise No_match;
     extern_optimal_prim_token scopes r r'
   with No_match ->
   try
     let r'' = flatten_application r' in
-    if !Flags.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print || !print_no_symbol then raise No_match;
     extern_symbol scopes vars r'' (uninterp_notations r'')
   with No_match -> match r' with
   | GRef (loc,ref) ->
@@ -764,7 +764,7 @@ and factorize_prod scopes vars na bk aty c =
   match na, c with
   | Name id, CProdN (loc,[nal,Default bk',ty],c)
       when binding_kind_eq bk bk' && constr_expr_eq aty ty
-      & not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
+      && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
       nal,c
   | _ ->
       [],c
@@ -774,7 +774,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
   match c with
   | CLambdaN (loc,[nal,Default bk',ty],c)
       when binding_kind_eq bk bk' && constr_expr_eq aty ty
-      & not (occur_name na ty) (* avoid na in ty escapes scope *) ->
+      && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
       nal,c
   | _ ->
       [],c
@@ -791,7 +791,7 @@ and extern_local_binder scopes vars = function
       let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
       (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
           (assums,ids,LocalRawAssum(nal,k,ty')::l)
-            when constr_expr_eq ty ty' &
+            when constr_expr_eq ty ty' &&
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ece2a45186..51c8e2e10a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -630,7 +630,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
     GVar (loc,id), make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
-  if Id.Set.mem id genv.ids or Id.Set.mem id ltacvars
+  if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars
   then
     GVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 624fa23aa0..a04631580e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -832,7 +832,7 @@ let browse_notation strict ntn map =
 let global_reference_of_notation test (ntn,(sc,c,_)) =
   match c with
   | NRef ref when test ref -> Some (ntn,sc,ref)
-  | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l & test ref ->
+  | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref ->
       Some (ntn,sc,ref)
   | _ -> None
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b571d03442..0e4cd80df4 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -151,14 +151,14 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
   | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
     when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
-    on_true_do (f ty1 ty2 & f c1 c2) add na1
+    on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
     when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
-      on_true_do (f ty1 ty2 & f c1 c2) add na1
+      on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GHole _, GHole _ -> true
   | GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2
   | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
-      on_true_do (f b1 b2 & f c1 c2) add na1
+      on_true_do (f b1 b2 && f c1 c2) add na1
   | (GCases _ | GRec _
     | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
   | _,(GCases _ | GRec _
@@ -315,8 +315,8 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) =
   let () = List.iter check foundrecbinding in
   let check_bound x =
     if not (List.mem x found) then
-      if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding
-	or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding
+      if List.mem_assoc x foundrec || List.mem_assoc x foundrecbinding
+        || list_rev_mem_assoc x foundrec || list_rev_mem_assoc x foundrecbinding
       then
 	error ((Id.to_string x)^" should not be bound in a recursive pattern of the right-hand side.")
       else
@@ -424,7 +424,7 @@ let rec subst_notation_constr subst bound raw =
                                (cpl',r'))
                         branches
       in
-        if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
+        if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &&
           rl' == rl && branches' == branches then raw else
           NCases (sty,rtntypopt',rl',branches')
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 43c79bd496..832af53317 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -264,7 +264,7 @@ let locs_of_notation loc locs ntn =
   let rec aux pos = function
     | [] -> if Int.equal pos el then [] else [(pos,el-1)]
     | (ba,ea)::l ->if Int.equal pos ba then aux ea l else (pos,ba-1)::aux ea l
-  in aux bl (Sort.list (fun l1 l2 -> fst l1 < fst l2) locs)
+  in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs)
 
 let ntn_loc loc (args,argslist,binderslist) =
   locs_of_notation loc