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
```
---
 pretyping/classops.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'pretyping/classops.ml')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 57dbfb2580..c12a236d8e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -195,7 +195,7 @@ let subst_cl_typ subst ct = match ct with
             pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
   | CL_IND i ->
       let i' = subst_ind subst i in
-	if i' == i then ct else CL_IND i'
+        if i' == i then ct else CL_IND i'
 
 (*CSC: here we should change the datatype for coercions: it should be possible
        to declare any term as a coercion *)
@@ -267,7 +267,7 @@ let lookup_path_between env sigma (s,t) =
   let (s,(t,p)) =
     apply_on_class_of env sigma s (fun i ->
       apply_on_class_of env sigma t (fun j ->
-	lookup_path_between_class (i,j))) in
+        lookup_path_between_class (i,j))) in
   (s,t,p)
 
 let lookup_path_to_fun_from env sigma s =
@@ -323,7 +323,7 @@ let warn_ambiguous_path =
 let different_class_params env i =
   let ci = class_info_from_index i in
     if (snd ci).cl_param > 0 then true
-    else 
+    else
       match fst ci with
       | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
       | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
@@ -351,16 +351,16 @@ let add_coercion_in_graph env sigma (ic,source,target) =
     ClPairMap.iter
       (fun (s,t) p ->
          if not (Bijint.Index.equal s t) then begin
-	   if Bijint.Index.equal t source then begin
+           if Bijint.Index.equal t source then begin
              try_add_new_path1 (s,target) (p@[ic]);
              ClPairMap.iter
-	       (fun (u,v) q ->
+               (fun (u,v) q ->
                   if not (Bijint.Index.equal u v) && Bijint.Index.equal u target &&  not (List.equal coe_info_typ_equal p q) then
-		    try_add_new_path1 (s,v) (p@[ic]@q))
+                    try_add_new_path1 (s,v) (p@[ic]@q))
                old_inheritance_graph
            end;
            if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p)
-	 end)
+         end)
       old_inheritance_graph
   end;
   match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
-- 
cgit v1.2.3