[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
```

1 files changed, 4 insertions, 4 deletions

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 9eb014aa62..21957b4775 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -41,9 +41,9 @@ val subst_glob_constr : env -> substitution -> glob_constr -> glob_constr
 
 val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g
 
-(** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr 
-   de Bruijn indexes are turned to bound names, avoiding names in [avoid] 
-   [isgoal] tells if naming must avoid global-level synonyms as intro does 
+(** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr
+   de Bruijn indexes are turned to bound names, avoiding names in [avoid]
+   [isgoal] tells if naming must avoid global-level synonyms as intro does
    [ctx] gives the names of the free variables *)
 
 val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> constr -> glob_constr
@@ -52,7 +52,7 @@ val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> con
 
 val detype_sort : evar_map -> Sorts.t -> glob_sort
 
-val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> 
+val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) ->
   evar_map -> rel_context -> 'a glob_decl_g list
 
 val share_pattern_names :