From d016f69818b30b75d186fb14f440b93b0518fc66 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 21 Nov 2019 15:38:39 +0100
Subject: [coq] Untabify the whole ML codebase.

We also remove trailing whitespace.

Script used:

```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
---
 lib/system.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'lib/system.ml')

diff --git a/lib/system.ml b/lib/system.ml
index 8c333ec267..2d68fd2fdf 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -29,9 +29,9 @@ let all_subdirs ~unix_path:root =
   let rec traverse path rel =
     let f = function
       | FileDir (path,f) ->
-	  let newrel = rel @ [f] in
-	  add path newrel;
-	  traverse path newrel
+          let newrel = rel @ [f] in
+          add path newrel;
+          traverse path newrel
       | _ -> ()
     in process_directory f path
   in
@@ -133,7 +133,7 @@ let find_file_in_path ?(warn=true) paths filename =
       root, filename
     else
       CErrors.user_err ~hdr:"System.find_file_in_path"
-	(hov 0 (str "Can't find file" ++ spc () ++ str filename))
+        (hov 0 (str "Can't find file" ++ spc () ++ str filename))
   else
     (* the name is considered to be the transcription as a relative
        physical name of a logical name, so we deal with it as a name
@@ -141,8 +141,8 @@ let find_file_in_path ?(warn=true) paths filename =
     try where_in_path ~warn paths filename
     with Not_found ->
       CErrors.user_err ~hdr:"System.find_file_in_path"
-	(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
-		str "on loadpath"))
+        (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
+                str "on loadpath"))
 
 let is_in_path lpath filename =
   try ignore (where_in_path ~warn:false lpath filename); true
-- 
cgit v1.2.3