Merge PR #11010: [coq] Untabify the whole ML codebase.

Reviewed-by: SkySkimmer
Reviewed-by: herbelin

5 files changed, 27 insertions, 27 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 09ecd675f7..ffb2928d55 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -155,24 +155,24 @@ let add_load_path (phys_path,coq_path) =
   let physical, logical = !load_paths in
     match List.filter2 (fun p d -> p = phys_path) physical logical with
       | _,[dir] ->
-	  if coq_path <> dir
+          if coq_path <> dir
             (* If this is not the default -I . to coqtop *)
             && not
             (phys_path = CUnix.canonical_path_name Filename.current_dir_name
-		&& coq_path = default_root_prefix)
-	  then
-	    begin
+                && coq_path = default_root_prefix)
+          then
+            begin
               (* Assume the user is concerned by library naming *)
-	      if dir <> default_root_prefix then
-		Feedback.msg_warning
-		  (str phys_path ++ strbrk " was previously bound to " ++
-		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
-		   pr_dirpath coq_path);
-	      remove_load_path phys_path;
-	      load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
-	    end
+              if dir <> default_root_prefix then
+                Feedback.msg_warning
+                  (str phys_path ++ strbrk " was previously bound to " ++
+                   pr_dirpath dir ++ strbrk "; it is remapped to " ++
+                   pr_dirpath coq_path);
+              remove_load_path phys_path;
+              load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+            end
       | _,[] ->
-	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+          load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
       | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^"."))
 
 let load_paths_of_dir_path dir =
diff --git a/checker/checker.ml b/checker/checker.ml
index d08e9e698d..5f93148be6 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -29,7 +29,7 @@ let parse_dir s =
     if n>=len then dirs else
     let pos =
       try
-	String.index_from s n '.'
+        String.index_from s n '.'
       with Not_found -> len
     in
     let dir = String.sub s n (pos-n) in
@@ -241,8 +241,8 @@ let explain_exn = function
       hov 0 (str "Stack overflow")
   | Match_failure(filename,pos1,pos2) ->
       hov 1 (anomaly_string () ++ str "Match failure in file " ++
-	     guill filename ++ str " at line " ++ int pos1 ++
-	     str " character " ++ int pos2 ++ report ())
+             guill filename ++ str " at line " ++ int pos1 ++
+             str " character " ++ int pos2 ++ report ())
   | Not_found ->
       hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
   | Failure s ->
@@ -312,12 +312,12 @@ let explain_exn = function
 
   | Assert_failure (s,b,e) ->
       hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
-	       (if s = "" then mt ()
-		else
-		  (str "(file \"" ++ str s ++ str "\", line " ++ int b ++
-		   str ", characters " ++ int e ++ str "-" ++
-		   int (e+6) ++ str ")")) ++
-	       report ())
+               (if s = "" then mt ()
+                else
+                  (str "(file \"" ++ str s ++ str "\", line " ++ int b ++
+                   str ", characters " ++ int e ++ str "-" ++
+                   int (e+6) ++ str ")")) ++
+               report ())
   | e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
 
 let deprecated flag =
@@ -333,8 +333,8 @@ let parse_args argv =
       indices_matter:=true; parse rem
 
     | "-coqlib" :: s :: rem ->
-      if not (exists_dir s) then 
-	fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
+      if not (exists_dir s) then
+        fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
       Envars.set_user_coqlib s;
       parse rem
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 3128e125dd..44b7089fd0 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -163,6 +163,6 @@ and check_signature env sign mp_mse res = match sign with
       MoreFunctor(arg_id,mtb,body)
   | NoFunctor struc ->
       let (_:env) = List.fold_left (fun env (lab,mb) ->
-	check_structure_field env mp_mse lab res mb) env struc
+        check_structure_field env mp_mse lab res mb) env struc
       in
       NoFunctor struc
diff --git a/checker/validate.ml b/checker/validate.ml
index 678af9f2d5..070a112bb6 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -105,7 +105,7 @@ and val_tuple ?name vs ctx o =
   else
     fail ctx o
       ("tuple size: found "^string_of_int (Obj.size o)^
-	  ", expected "^string_of_int n)
+          ", expected "^string_of_int n)
 
 (* Check that the object is either a constant constructor of tag < cc,
    or a constructed variant. each element of vv is an array of
diff --git a/checker/values.ml b/checker/values.ml
index 3882f88391..56321a27ff 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -117,7 +117,7 @@ let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|]
 
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
 
-let v_boollist = List v_bool  
+let v_boollist = List v_bool
 
 let v_caseinfo =
   let v_cstyle = v_enum "case_style" 5 in