From 826eb7c6d11007dfd747d49852e71a22e0a3850a Mon Sep 17 00:00:00 2001
From: xclerc
Date: Thu, 19 Sep 2013 12:59:04 +0000
Subject: 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
---
 tools/coqdep_common.ml |  8 ++++----
 tools/coqmktop.ml      | 10 +++++-----
 2 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 41b026c43d..8c5e5b1ee4 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -265,10 +265,10 @@ let escape =
     Buffer.clear s';
     for i = 0 to String.length s - 1 do
       let c = s.[i] in
-      if c = ' ' or c = '#' or c = ':' (* separators and comments *)
-	or c = '%' (* pattern *)
-	or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *)
-	or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 
+      if c = ' ' || c = '#' || c = ':' (* separators and comments *)
+        || c = '%' (* pattern *)
+	|| c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *)
+	|| i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 
 	    'A' <= s.[1] && s.[1] <= 'Z' || 
 	    'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
       then begin
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 0ab732da21..0bcd44d0eb 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -190,11 +190,11 @@ let parse_args () =
     | ("-no-start") :: rem -> no_start:=true; parse (op, fl) rem
     | f :: rem ->
 	if Filename.check_suffix f ".ml"
-	  or Filename.check_suffix f ".cmx"
-	  or Filename.check_suffix f ".cmo"
-	  or Filename.check_suffix f ".cmxa"
-	  or Filename.check_suffix f ".cma"
-	  or Filename.check_suffix f ".c" then
+          || Filename.check_suffix f ".cmx"
+	  || Filename.check_suffix f ".cmo"
+	  || Filename.check_suffix f ".cmxa"
+	  || Filename.check_suffix f ".cma"
+	  || Filename.check_suffix f ".c" then
 	    parse (op,f::fl) rem
 	else begin
 	  prerr_endline ("Don't know what to do with " ^ f);
-- 
cgit v1.2.3