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

13 files changed, 192 insertions, 192 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 46a80239cf..150dad16c2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -463,16 +463,16 @@ let test_constr_universes env sigma leq m n =
       if Sorts.equal s1 s2 then true
       else (cstrs := Set.add
               (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
-	    true)
+            true)
     in
-    let leq_sorts s1 s2 = 
+    let leq_sorts s1 s2 =
       let s1 = ESorts.kind sigma s1 in
       let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
-      else 
+      else
         (cstrs := Set.add
            (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
-	 true)
+         true)
     in
     let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in
     let res =
@@ -496,20 +496,20 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   let kind c = kind sigma c in
   match kind m, kind n with
   | Proj (p, c), App (f, args)
-  | App (f, args), Proj (p, c) -> 
+  | App (f, args), Proj (p, c) ->
       (match kind f with
-      | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
+      | Const (p', u) when Constant.equal (Projection.constant p) p' ->
           let npars = Projection.npars p in
           if Array.length args == npars + 1 then
             eqc' 0 c args.(npars)
-	  else false
+          else false
       | _ -> false)
   | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n
 
 let eq_constr_universes_proj env sigma m n =
   let open UnivProblem in
   if m == n then Some Set.empty
-  else 
+  else
     let cstrs = ref Set.empty in
     let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
     let eq_sorts s1 s2 =
@@ -519,7 +519,7 @@ let eq_constr_universes_proj env sigma m n =
       else
         (cstrs := Set.add
            (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
-	 true)
+         true)
     in
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 5444d88e47..b09cc87f97 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -562,19 +562,19 @@ let rec check_and_clear_in_constr env evdref err ids global c =
         c
 
       | Evar (evk,l as ev) ->
-	  if Evd.is_defined !evdref evk then
-	    (* If evk is already defined we replace it by its definition *)
+          if Evd.is_defined !evdref evk then
+            (* If evk is already defined we replace it by its definition *)
             let nc = Evd.existential_value !evdref (EConstr.of_existential ev) in
             let nc = EConstr.Unsafe.to_constr nc in
-	      (check_and_clear_in_constr env evdref err ids global nc)
-	  else
-	    (* We check for dependencies to elements of ids in the
-	       evar_info corresponding to e and in the instance of
-	       arguments. Concurrently, we build a new evar
-	       corresponding to e where hypotheses of ids have been
-	       removed *)
-	    let evi = Evd.find_undefined !evdref evk in
-	    let ctxt = Evd.evar_filtered_context evi in
+              (check_and_clear_in_constr env evdref err ids global nc)
+          else
+            (* We check for dependencies to elements of ids in the
+               evar_info corresponding to e and in the instance of
+               arguments. Concurrently, we build a new evar
+               corresponding to e where hypotheses of ids have been
+               removed *)
+            let evi = Evd.find_undefined !evdref evk in
+            let ctxt = Evd.evar_filtered_context evi in
             let (rids,filter) =
               List.fold_right2
                 (fun h a (ri,filter) ->
@@ -594,11 +594,11 @@ let rec check_and_clear_in_constr env evdref err ids global c =
                   (* No dependency at all, we can keep this ev's context hyp *)
                     (ri, true::filter)
                   with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter))
-		ctxt (Array.to_list l) (Id.Map.empty,[]) in
-	    (* Check if some rid to clear in the context of ev has dependencies
-	       in the type of ev and adjust the source of the dependency *)
-	    let _nconcl =
-	      try
+                ctxt (Array.to_list l) (Id.Map.empty,[]) in
+            (* Check if some rid to clear in the context of ev has dependencies
+               in the type of ev and adjust the source of the dependency *)
+            let _nconcl =
+              try
                 let nids = Id.Map.domain rids in
                 let global = Id.Set.exists is_section_variable nids in
                 let concl = EConstr.Unsafe.to_constr (evar_concl evi) in
@@ -694,7 +694,7 @@ let gather_dependent_evars q evm =
     let (is_dependent,e) = Queue.pop q in
     (* checks if [e] has already been added to [!acc] *)
     begin if not (Evar.Map.mem e !acc) then
-        acc := process_dependent_evar q !acc evm is_dependent e  
+        acc := process_dependent_evar q !acc evm is_dependent e
     end
   done;
   !acc
@@ -736,7 +736,7 @@ let undefined_evars_of_term evd t =
     match EConstr.kind evd c with
       | Evar (n, l) ->
         let acc = Evar.Set.add n acc in
-	Array.fold_left evrec acc l
+        Array.fold_left evrec acc l
       | _ -> EConstr.fold evd evrec acc c
   in
   evrec Evar.Set.empty t
@@ -751,10 +751,10 @@ let undefined_evars_of_evar_info evd evi =
   Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
     (Evar.Set.union
        (match evi.evar_body with
-	 | Evar_empty -> Evar.Set.empty
+         | Evar_empty -> Evar.Set.empty
          | Evar_defined b -> undefined_evars_of_term evd b)
        (undefined_evars_of_named_context evd
-	  (named_context_of_val evi.evar_hyps)))
+          (named_context_of_val evi.evar_hyps)))
 
 type undefined_evars_cache = {
   mutable cache : (EConstr.named_declaration * Evar.Set.t) ref Id.Map.t;
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 7877b94582..65a069a280 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -58,7 +58,7 @@ val new_pure_evar :
 
 val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
 
-(** Create a new Type existential variable, as we keep track of 
+(** Create a new Type existential variable, as we keep track of
     them during type-checking and unification. *)
 val new_type_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
diff --git a/engine/evd.ml b/engine/evd.ml
index f051334f69..94868d9bdd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -652,7 +652,7 @@ let existential_type0 = existential_type
 let add_constraints d c =
   { d with universes = UState.add_constraints d.universes c }
 
-let add_universe_constraints d c = 
+let add_universe_constraints d c =
   { d with universes = UState.add_universe_constraints d.universes c }
 
 (*** /Lifting... ***)
@@ -664,7 +664,7 @@ let is_empty d =
   List.is_empty d.conv_pbs &&
   Metamap.is_empty d.metas
 
-let cmap f evd = 
+let cmap f evd =
   { evd with
       metas = Metamap.map (map_clb f) evd.metas;
       defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
@@ -701,7 +701,7 @@ let empty = {
   extras = Store.empty;
 }
 
-let from_env e = 
+let from_env e =
   { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) }
 
 let from_ctx ctx = { empty with universes = ctx }
@@ -711,7 +711,7 @@ let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
   let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
   let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
-  let universes = 
+  let universes =
     if not with_univs then evd.universes
     else UState.union evd.universes d.universes
   in
@@ -812,10 +812,10 @@ let extract_conv_pbs evd p =
   let (pbs,pbs1) =
     List.fold_left
       (fun (pbs,pbs1) pb ->
-    	 if p pb then
-	   (pb::pbs,pbs1)
+         if p pb then
+           (pb::pbs,pbs1)
          else
-	   (pbs,pb::pbs1))
+           (pbs,pb::pbs1))
       ([],[])
       evd.conv_pbs
   in
@@ -866,7 +866,7 @@ let universe_subst evd =
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
   {evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'}
 
-let merge_universe_subst evd subst = 
+let merge_universe_subst evd subst =
   {evd with universes = UState.merge_subst evd.universes subst }
 
 let with_context_set ?loc rigid d (a, ctx) =
@@ -915,7 +915,7 @@ let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
 
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
-let is_flexible_level evd l = 
+let is_flexible_level evd l =
   let uctx = evd.universes in
     Univ.LMap.mem l (UState.subst uctx)
 
@@ -947,7 +947,7 @@ let normalize_universe_instance evd l =
 let normalize_sort evars s =
   match s with
   | SProp | Prop | Set -> s
-  | Type u -> 
+  | Type u ->
     let u' = normalize_universe evars u in
     if u' == u then s else Sorts.sort_of_univ u'
 
@@ -974,7 +974,7 @@ let set_eq_instances ?(flex=false) d u1 u2 =
     (UnivProblem.enforce_eq_instances_univs flex u1 u2 UnivProblem.Set.empty)
 
 let set_leq_sort env evd s1 s2 =
-  let s1 = normalize_sort evd s1 
+  let s1 = normalize_sort evd s1
   and s2 = normalize_sort evd s2 in
   match is_eq_sort s1 s2 with
   | None -> evd
@@ -982,7 +982,7 @@ let set_leq_sort env evd s1 s2 =
      if not (type_in_type env) then
        add_universe_constraints evd (UnivProblem.Set.singleton (UnivProblem.ULe (u1,u2)))
      else evd
-	    
+
 let check_eq evd s s' =
   UGraph.check_eq (UState.ugraph evd.universes) s s'
 
@@ -1256,7 +1256,7 @@ type 'a sigma = {
 
 let sig_it x = x.it
 let sig_sig x = x.sigma
-let on_sig s f = 
+let on_sig s f =
   let sigma', v = f s.sigma in
     { s with sigma = sigma' }, v
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 5ab53947f7..7876e9a48f 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -141,7 +141,7 @@ val empty : evar_map
 (** The empty evar map. *)
 
 val from_env : env -> evar_map
-(** The empty evar map with given universe context, taking its initial 
+(** The empty evar map with given universe context, taking its initial
     universes from env. *)
 
 val from_ctx : UState.t -> evar_map
@@ -251,7 +251,7 @@ val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info
 
 val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
 
-val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool -> 
+val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
   evar_map ->  evar_map -> evar_map
 (** spiwack: this function seems to somewhat break the abstraction. *)
 
@@ -596,8 +596,8 @@ val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_
 val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
 (** See [UState.make_nonalgebraic_variable]. *)
 
-val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option 
-(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
+val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option
+(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
     not a local sort variable declared in [evm] *)
 
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
@@ -610,7 +610,7 @@ val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
 val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
 val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
-val set_eq_instances : ?flex:bool -> 
+val set_eq_instances : ?flex:bool ->
   evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map
 
 val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
diff --git a/engine/namegen.ml b/engine/namegen.ml
index b850f38b4d..56277e8092 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -153,15 +153,15 @@ let hdchar env sigma c =
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar (ESorts.kind sigma s)
     | Rel n ->
-	(if n<=k then "p" (* the initial term is flexible product/function *)
-	 else
+        (if n<=k then "p" (* the initial term is flexible product/function *)
+         else
            try match let d = lookup_rel (n-k) env in get_name d, get_type d with
              | Name id, _ -> lowercase_first_char id
              | Anonymous, t -> hdrec 0 (lift (n-k) t)
-	   with Not_found -> "y")
+           with Not_found -> "y")
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
         let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in
-	lowercase_first_char id
+        lowercase_first_char id
     | Evar _ (* We could do better... *)
     | Meta _ | Case (_, _, _, _) -> "y"
     | Int _ -> "i"
@@ -196,7 +196,7 @@ let name_context env sigma hyps =
   snd
     (List.fold_left
        (fun (env,hyps) d ->
-	  let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps))
+          let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps))
        (env,[]) (List.rev hyps))
 
 let mkProd_or_LetIn_name env sigma b d = mkProd_or_LetIn (name_assumption env sigma d) b
@@ -356,8 +356,8 @@ let next_name_away_with_default_using_types default na avoid t =
   let id = match na with
     | Name id -> id
     | Anonymous -> match !reserved_type_name t with
-	| Name id -> id
-	| Anonymous -> Id.of_string default in
+        | Name id -> id
+        | Anonymous -> Id.of_string default in
   next_ident_away id avoid
 
 let next_name_away = next_name_away_with_default default_non_dependent_string
@@ -458,12 +458,12 @@ let rename_bound_vars_as_displayed sigma avoid env c =
   let rec rename avoid env c =
     match EConstr.kind sigma c with
     | Prod (na,c1,c2)  ->
-	let na',avoid' =
+        let na',avoid' =
           compute_displayed_name_in sigma
             (RenamingElsewhereFor (env,c2)) avoid na.binder_name c2 in
         mkProd ({na with binder_name=na'}, c1, rename avoid' (na' :: env) c2)
     | LetIn (na,c1,t,c2) ->
-	let na',avoid' =
+        let na',avoid' =
           compute_displayed_let_name_in sigma
             (RenamingElsewhereFor (env,c2)) avoid na.binder_name c2 in
         mkLetIn ({na with binder_name=na'},c1,t, rename avoid' (na' :: env) c2)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 7a8544f2d6..4a1cd4d44f 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -88,7 +88,7 @@ val next_ident_away : Id.t -> Id.Set.t -> Id.t
 (** Avoid clashing with a name already used in current module *)
 val next_ident_away_in_goal : Id.t -> Id.Set.t -> Id.t
 
-(** Avoid clashing with a name already used in current module 
+(** Avoid clashing with a name already used in current module
    but tolerate overwriting section variables, as in goals *)
 val next_global_ident_away : Id.t -> Id.Set.t -> Id.t
 
diff --git a/engine/nameops.ml b/engine/nameops.ml
index baa19050d7..fe0a91e3ba 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -72,13 +72,13 @@ let cut_ident skip_quote s =
     else
       let c = Char.code (String.get s (n-1)) in
       if Int.equal c code_of_0 && not (Int.equal n slen) then
-	numpart (n-1) n'
+        numpart (n-1) n'
       else if code_of_0 <= c && c <= code_of_9 then
-	numpart (n-1) (n-1)
+        numpart (n-1) (n-1)
       else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then
-	numpart (n-1) (n-1)
+        numpart (n-1) (n-1)
       else
-	n'
+        n'
   in
   numpart slen slen
 
@@ -126,20 +126,20 @@ let increment_subscript id =
     let c = id.[carrypos] in
     if is_digit c then
       if Int.equal (Char.code c) (Char.code '9') then begin
-	assert (carrypos>0);
-	add (carrypos-1)
+        assert (carrypos>0);
+        add (carrypos-1)
       end
       else begin
-	let newid = Bytes.of_string id in
-	Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
-	Bytes.set newid carrypos (Char.chr (Char.code c + 1));
-	newid
+        let newid = Bytes.of_string id in
+        Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+        Bytes.set newid carrypos (Char.chr (Char.code c + 1));
+        newid
       end
     else begin
       let newid = Bytes.of_string (id^"0") in
       if carrypos < len-1 then begin
-	Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
-	Bytes.set newid (carrypos+1) '1'
+        Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+        Bytes.set newid (carrypos+1) '1'
       end;
       newid
     end
diff --git a/engine/proofview.ml b/engine/proofview.ml
index d6f5aab1d1..ed44372045 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -130,7 +130,7 @@ let focus_context (left,right) =
     i]. *)
 let focus_sublist i j l =
   let (left,sub_right) = CList.goto (i-1) l in
-  let (sub, right) = 
+  let (sub, right) =
     try CList.chop (j-i+1) sub_right
     with Failure _ -> raise CList.IndexOutOfRange
   in
@@ -479,7 +479,7 @@ let fold_left2_goal i s l =
   let err =
     return () >>= fun () -> (* Delay the computation of list lengths. *)
     tclZERO (SizeMismatch (CList.length initial.comb,CList.length l))
-  in 
+  in
   Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
     Solution.get >>= fun step ->
     match cleared_alias step goal with
@@ -515,7 +515,7 @@ let fold_left2_goal i s l =
 let tclDISPATCHGEN0 join tacs =
   match tacs with
   | [] ->
-      begin 
+      begin
         let open Proof in
         Comb.get >>= function
         | [] -> tclUNIT (join [])
@@ -1012,7 +1012,7 @@ module Unsafe = struct
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
-  let tclEVARUNIVCONTEXT ctx = 
+  let tclEVARUNIVCONTEXT ctx =
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
 
   let reset_future_goals p =
@@ -1229,7 +1229,7 @@ module V82 = struct
     let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in
     { ps with solution = evd; }
     end
-      
+
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
 
@@ -1238,8 +1238,8 @@ module V82 = struct
     let undef = Evd.undefined_map pv.solution in
     let goals = CList.rev_map fst (Evar.Map.bindings undef) in
     { pv with comb = List.map with_empty_state goals }
-      
-    
+
+
 
   let top_goals initial { solution=solution; } =
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 764a4a0058..8ec53ac78c 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -145,7 +145,7 @@ val unfocus : focus_context -> proofview -> proofview
 
 
 (** The abstract type of tactics *)
-type +'a tactic 
+type +'a tactic
 
 (** Applies a tactic to the current proofview. Returns a tuple
     [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv]
@@ -170,7 +170,7 @@ val apply
 
 (** Unit of the tactic monad. *)
 val tclUNIT : 'a -> 'a tactic
- 
+
 (** Bind operation of the tactic monad. *)
 val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
 
@@ -440,7 +440,7 @@ module Unsafe : sig
       goal. If goals have been solved in [sigma] they will still
       appear as unsolved goals. *)
   val tclEVARS : Evd.evar_map -> unit tactic
-    
+
   (** Like {!tclEVARS} but also checks whether goals have been solved. *)
   val tclEVARSADVANCE : Evd.evar_map -> unit tactic
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 90fa8546ce..a65b8275e6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -95,15 +95,15 @@ let pr_meta_map env sigma =
     | _ -> mt() in
   let pr_meta_binding = function
     | (mv,Cltyp (na,b)) ->
-      	hov 0
-	  (pr_meta mv ++ pr_name na ++ str " : " ++
+        hov 0
+          (pr_meta mv ++ pr_name na ++ str " : " ++
            print_constr env sigma b.rebus ++ fnl ())
     | (mv,Clval(na,(b,s),t)) ->
-      	hov 0
-	  (pr_meta mv ++ pr_name na ++ str " := " ++
+        hov 0
+          (pr_meta mv ++ pr_name na ++ str " := " ++
            print_constr env sigma b.rebus ++
            str " : " ++ print_constr env sigma t.rebus ++
-	   spc () ++ pr_instance_status s ++ fnl ())
+           spc () ++ pr_instance_status s ++ fnl ())
   in
   prlist pr_meta_binding (meta_list sigma)
 
@@ -232,7 +232,7 @@ let pr_evar_universe_context ctx =
   let prl = pr_uctx_level ctx in
   if UState.is_empty ctx then mt ()
   else
-    (str"UNIVERSES:"++brk(0,1)++ 
+    (str"UNIVERSES:"++brk(0,1)++
        h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
      h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
@@ -387,10 +387,10 @@ let pr_var_decl env decl =
   let pbody = match decl with
     | LocalAssum _ ->  mt ()
     | LocalDef (_,c,_) ->
-	(* Force evaluation *)
-	let c = EConstr.of_constr c in
+        (* Force evaluation *)
+        let c = EConstr.of_constr c in
         let pb = print_constr_env env sigma c in
-	  (str" := " ++ pb ++ cut () ) in
+          (str" := " ++ pb ++ cut () ) in
   let pt = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in
   let ptyp = (str" : " ++ pt) in
     (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp))
@@ -401,10 +401,10 @@ let pr_rel_decl env decl =
   let pbody = match decl with
     | LocalAssum _ -> mt ()
     | LocalDef (_,c,_) ->
-	(* Force evaluation *)
-	let c = EConstr.of_constr c in
+        (* Force evaluation *)
+        let c = EConstr.of_constr c in
         let pb = print_constr_env env sigma c in
-	  (str":=" ++ spc () ++ pb ++ spc ()) in
+          (str":=" ++ spc () ++ pb ++ spc ()) in
   let ptyp = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in
     match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
@@ -412,13 +412,13 @@ let pr_rel_decl env decl =
 
 let print_named_context env =
   hv 0 (fold_named_context
-	  (fun env d pps ->
-	    pps ++ ws 2 ++ pr_var_decl env d)
+          (fun env d pps ->
+            pps ++ ws 2 ++ pr_var_decl env d)
           env ~init:(mt ()))
 
 let print_rel_context env =
   hv 0 (fold_rel_context
-	  (fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d)
+          (fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d)
           env ~init:(mt ()))
 
 let print_env env =
@@ -426,7 +426,7 @@ let print_env env =
     fold_named_context
       (fun env d pps ->
          let pidt =  pr_var_decl env d in
-	 (pps ++ fnl () ++ pidt))
+         (pps ++ fnl () ++ pidt))
       env ~init:(mt ())
   in
   let db_env =
@@ -517,9 +517,9 @@ let it_mkLambda_or_LetIn_from_no_LetIn c decls =
 let rec strip_head_cast sigma c = match EConstr.kind sigma c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 = match EConstr.kind sigma f with
-	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-	| Cast (c,_,_) -> collapse_rec c cl2
-	| _ -> if Int.equal (Array.length cl2) 0 then f else EConstr.mkApp (f,cl2)
+        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+        | Cast (c,_,_) -> collapse_rec c cl2
+        | _ -> if Int.equal (Array.length cl2) 0 then f else EConstr.mkApp (f,cl2)
       in
       collapse_rec f cl
   | Cast (c,_,_) -> strip_head_cast sigma c
@@ -531,7 +531,7 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with
   | App (f,args) when EConstr.isEvar sigma (Array.last args) ->
       let open EConstr in
       drop_extra_implicit_args sigma
-	(mkApp (f,fst (Array.chop (Array.length args - 1) args)))
+        (mkApp (f,fst (Array.chop (Array.length args - 1) args)))
   | _ -> c
 
 (* Get the last arg of an application *)
@@ -601,27 +601,27 @@ let map_constr_with_binders_left_to_right sigma g f l c =
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _ | Int _ | Float _) -> c
-  | Cast (b,k,t) -> 
-    let b' = f l b in 
+  | Cast (b,k,t) ->
+    let b' = f l b in
     let t' = f l t in
       if b' == b && t' == t then c
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
       let b' = f (g (LocalAssum (na,t)) l) b in
-	if t' == t && b' == b then c
-	else mkProd (na, t', b')
+        if t' == t && b' == b then c
+        else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
       let b' = f (g (LocalAssum (na,t)) l) b in
-	if t' == t && b' == b then c
-	else mkLambda (na, t', b')
+        if t' == t && b' == b then c
+        else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
       let b' = f (g (LocalDef (na,bo,t)) l) b in
-	if bo' == bo && t' == t && b' == b then c
-	else mkLetIn (na, bo', t', b')	    
+        if bo' == bo && t' == t && b' == b then c
+        else mkLetIn (na, bo', t', b')
   | App (c,[||]) -> assert false
   | App (t,al) ->
       (*Special treatment to be able to recognize partially applied subterms*)
@@ -629,13 +629,13 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       let app = (mkApp (t, Array.sub al 0 (Array.length al - 1))) in
       let app' = f l app in
       let a' = f l a in
-	if app' == app && a' == a then c
-	else mkApp (app', [| a' |])
+        if app' == app && a' == a then c
+        else mkApp (app', [| a' |])
   | Proj (p,b) ->
     let b' = f l b in
       if b' == b then c
       else mkProj (p, b')
-  | Evar (e,al) -> 
+  | Evar (e,al) ->
     let al' = Array.map_left (f l) al in
       if Array.for_all2 (==) al' al then c
       else mkEvar (e, al')
@@ -644,20 +644,20 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       let b' = f l b in
       let p' = f l p in
       let bl' = Array.map_left (f l) bl in
-	if b' == b && p' == p && bl' == bl then c
-	else mkCase (ci, p', b', bl')
+        if b' == b && p' == p && bl' == bl then c
+        else mkCase (ci, p', b', bl')
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
-	if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
-	then c
-	else mkFix (ln,(lna,tl',bl'))
+        if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+        then c
+        else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
-	if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
-	then c
-	else mkCoFix (ln,(lna,tl',bl'))
+        if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+        then c
+        else mkCoFix (ln,(lna,tl',bl'))
 
 let map_under_context_with_full_binders sigma g f l n d =
   let open EConstr in
@@ -703,9 +703,9 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
       let c' = f l c in
       let al' = Array.map (f l) al in
       if c==c' && Array.for_all2 (==) al al' then cstr else mkApp (c', al')
-  | Proj (p,c) -> 
+  | Proj (p,c) ->
       let c' = f l c in
-	if c' == c then cstr else mkProj (p, c')
+        if c' == c then cstr else mkProj (p, c')
   | Evar (e,al) ->
       let al' = Array.map (f l) al in
       if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
@@ -867,14 +867,14 @@ let dependent_main noevar sigma m t =
       raise Occur
     else
       match EConstr.kind sigma m, EConstr.kind sigma t with
-	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+        | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+            deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
             Array.Fun1.iter deprec m
-	      (Array.sub lt
-		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
-	| _, Evar _ when noevar -> ()
-	| _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t
+              (Array.sub lt
+                (Array.length lm) ((Array.length lt) - (Array.length lm)))
+        | _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
+        | _, Evar _ when noevar -> ()
+        | _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t
   in
   try deprec m t; false with Occur -> true
 
@@ -895,14 +895,14 @@ let count_occurrences sigma m t =
       incr n
     else
       match EConstr.kind sigma m, EConstr.kind sigma t with
-	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
-	    Array.iter (countrec m)
-	      (Array.sub lt
-		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when isMeta sigma c -> ()
-	| _, Evar _ -> ()
-	| _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t
+        | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+            countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+            Array.iter (countrec m)
+              (Array.sub lt
+                (Array.length lm) ((Array.length lt) - (Array.length lm)))
+        | _, Cast (c,_,_) when isMeta sigma c -> ()
+        | _, Evar _ -> ()
+        | _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t
   in
   countrec m t;
   !n
@@ -949,13 +949,13 @@ let prefix_application sigma eq_fun (k,c) t =
   let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
   match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
-	let l1 = Array.length cl1
-	and l2 = Array.length cl2 in
-	if l1 <= l2
-	   && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
-	else
-	  None
+        let l1 = Array.length cl1
+        and l2 = Array.length cl2 in
+        if l1 <= l2
+           && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+          Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+        else
+          None
     | _ -> None
 
 let my_prefix_application sigma eq_fun (k,c) by_c t =
@@ -963,13 +963,13 @@ let my_prefix_application sigma eq_fun (k,c) by_c t =
   let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
   match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
-	let l1 = Array.length cl1
-	and l2 = Array.length cl2 in
-	if l1 <= l2
-	   && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
-	else
-	  None
+        let l1 = Array.length cl1
+        and l2 = Array.length cl2 in
+        if l1 <= l2
+           && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+          Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+        else
+          None
     | _ -> None
 
 (* Recognizing occurrences of a given subterm in a term: [subst_term c t]
@@ -1002,7 +1002,7 @@ let replace_term_gen sigma eq_fun c by_c in_t =
       | None ->
     (if eq_fun sigma c t then (EConstr.Vars.lift k by_c) else
       EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c))
-	substrec kc t)
+        substrec kc t)
   in
   substrec (0,c) in_t
 
@@ -1127,7 +1127,7 @@ let compare_constr_univ sigma f cv_pb t1 t2 =
   match EConstr.kind sigma t1, EConstr.kind sigma t2 with
       Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2)
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
-	f Reduction.CONV t1 t2 && f cv_pb c1 c2
+        f Reduction.CONV t1 t2 && f cv_pb c1 c2
     | Const (c, u), Const (c', u') -> Constant.equal c c'
     | Ind (i, _), Ind (i', _) -> eq_ind i i'
     | Construct (i, _), Construct (i', _) -> eq_constructor i i'
@@ -1145,9 +1145,9 @@ let split_app sigma c = match EConstr.kind sigma c with
     App(c,l) ->
       let len = Array.length l in
       if Int.equal len 0 then ([],c) else
-	let last = Array.get l (len-1) in
-	let prev = Array.sub l 0 (len-1) in
-	c::(Array.to_list prev), last
+        let last = Array.get l (len-1) in
+        let prev = Array.sub l 0 (len-1) in
+        c::(Array.to_list prev), last
   | _ -> assert false
 
 type subst = (EConstr.rel_context * EConstr.constr) Evar.Map.t
@@ -1177,15 +1177,15 @@ let filtering sigma env cv_pb c1 c2 =
         | _ -> assert false
         end
       | Prod (n,t1,c1), Prod (_,t2,c2) ->
-	  aux env cv_pb t1 t2;
-	  aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2
+          aux env cv_pb t1 t2;
+          aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
-	  if compare_constr_univ sigma
-	  (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
-	  else raise CannotFilter
-	  (* TODO: le reste des binders *)
+          if compare_constr_univ sigma
+          (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
+          else raise CannotFilter
+          (* TODO: le reste des binders *)
   in
   aux env cv_pb c1 c2; !evm
 
@@ -1241,18 +1241,18 @@ let rec eta_reduce_head sigma c =
   let open Vars in
   match EConstr.kind sigma c with
     | Lambda (_,c1,c') ->
-	(match EConstr.kind sigma (eta_reduce_head sigma c') with
+        (match EConstr.kind sigma (eta_reduce_head sigma c') with
            | App (f,cl) ->
                let lastn = (Array.length cl) - 1 in
                if lastn < 0 then anomaly (Pp.str "application without arguments.")
                else
                  (match EConstr.kind sigma cl.(lastn) with
                     | Rel 1 ->
-			let c' =
+                        let c' =
                           if Int.equal lastn 0 then f
-			  else mkApp (f, Array.sub cl 0 lastn)
-			in
-			if noccurn sigma 1 c'
+                          else mkApp (f, Array.sub cl 0 lastn)
+                        in
+                        if noccurn sigma 1 c'
                         then lift (-1) c'
                         else c
                     | _   -> c)
@@ -1278,9 +1278,9 @@ let assums_of_rel_context sign =
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
     | d::sign ->
-	aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign
+        aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign
     | [] ->
-	acc
+        acc
   in
   aux env [] (List.rev sign)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index ba17cdde93..3546ece581 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -15,7 +15,7 @@ open Names
 open Univ
 
 module UNameMap = Names.Id.Map
-    
+
 type uinfo = {
   uname : Id.t option;
   uloc : Loc.t option;
@@ -93,12 +93,12 @@ let union ctx ctx' =
       { uctx_names = (names, names_rev);
         uctx_local = local;
         uctx_seff_univs = seff;
-        uctx_univ_variables = 
+        uctx_univ_variables =
           LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
-        uctx_univ_algebraic = 
+        uctx_univ_algebraic =
           LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
         uctx_initial_universes = declarenew ctx.uctx_initial_universes;
-        uctx_universes = 
+        uctx_universes =
           (if local == ctx.uctx_local then ctx.uctx_universes
            else
              let cstrsr = ContextSet.constraints ctx'.uctx_local in
@@ -234,7 +234,7 @@ let process_universe_constraints ctx cstrs =
   let unify_universes cst local =
     let cst = nf_constraint cst in
       if UnivProblem.is_trivial cst then local
-      else 
+      else
           match cst with
           | ULe (l, r) ->
             begin match Univ.Universe.level r with
@@ -273,7 +273,7 @@ let process_universe_constraints ctx cstrs =
             if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local
           | UEq (l, r) -> equalize_universes l r local
   in
-  let local = 
+  let local =
     UnivProblem.Set.fold unify_universes cstrs Constraint.empty
   in
     !vars, !weak, local
@@ -326,9 +326,9 @@ let constrain_variables diff ctx =
       diff (univs, ctx.uctx_univ_variables, local)
   in
   { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
-  
+
 let qualid_of_level uctx =
-  let map, map_rev = uctx.uctx_names in 
+  let map, map_rev = uctx.uctx_names in
     fun l ->
       try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
       with Not_found | Option.IsNone ->
@@ -463,7 +463,7 @@ let restrict ctx vars =
   let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
-type rigid = 
+type rigid =
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
 
@@ -558,20 +558,20 @@ let new_univ_variable ?loc rigid name
   let uctx', pred =
     match rigid with
     | UnivRigid -> uctx, true
-    | UnivFlexible b -> 
+    | UnivFlexible b ->
       let uvars' = LMap.add u None uvars in
         if b then {uctx with uctx_univ_variables = uvars';
           uctx_univ_algebraic = LSet.add u avars}, false
         else {uctx with uctx_univ_variables = uvars'}, false
   in
-  let names = 
+  let names =
     match name with
     | Some n -> add_uctx_names ?loc n u uctx.uctx_names
     | None -> add_uctx_loc u loc uctx.uctx_names
   in
   let initial =
     UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes
-  in                                                 
+  in
   let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
                 uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false
@@ -590,7 +590,7 @@ let add_global_univ uctx u =
   let initial =
     UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
   in
-  let univs = 
+  let univs =
     UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
   in
   { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
@@ -631,11 +631,11 @@ let make_nonalgebraic_variable ctx u =
 let make_flexible_nonalgebraic ctx =
   {ctx with uctx_univ_algebraic = LSet.empty}
 
-let is_sort_variable uctx s = 
-  match s with 
-  | Sorts.Type u -> 
+let is_sort_variable uctx s =
+  match s with
+  | Sorts.Type u ->
     (match universe_level u with
-    | Some l as x -> 
+    | Some l as x ->
         if LSet.mem l (ContextSet.levels uctx.uctx_local) then x
         else None
     | None -> None)
@@ -673,7 +673,7 @@ let normalize_variables uctx =
       uctx_universes = univs }
 
 let abstract_undefined_variables uctx =
-  let vars' = 
+  let vars' =
     LMap.fold (fun u v acc ->
       if v == None then LSet.remove u acc
       else acc)
@@ -682,11 +682,11 @@ let abstract_undefined_variables uctx =
       uctx_univ_algebraic = vars' }
 
 let fix_undefined_variables uctx =
-  let algs', vars' = 
+  let algs', vars' =
     LMap.fold (fun u v (algs, vars as acc) ->
       if v == None then (LSet.remove u algs, LMap.remove u vars)
       else acc)
-      uctx.uctx_univ_variables 
+      uctx.uctx_univ_variables
       (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
   in
   { uctx with uctx_univ_variables = vars';
@@ -698,7 +698,7 @@ let refresh_undefined_univ_variables uctx =
   let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc)
     uctx.uctx_univ_algebraic LSet.empty
   in
-  let vars = 
+  let vars =
     LMap.fold
       (fun u v acc ->
         LMap.add (subst_fn u)
@@ -736,14 +736,14 @@ let minimize uctx =
       { uctx_names = uctx.uctx_names;
         uctx_local = us';
         uctx_seff_univs = uctx.uctx_seff_univs; (* not sure about this *)
-        uctx_univ_variables = vars'; 
+        uctx_univ_variables = vars';
         uctx_univ_algebraic = algs';
         uctx_universes = universes;
         uctx_universes_lbound = lbound;
         uctx_initial_universes = uctx.uctx_initial_universes;
         uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) }
 
-let universe_of_name uctx s = 
+let universe_of_name uctx s =
   UNameMap.find s (fst uctx.uctx_names)
 
 let pr_weak prl {uctx_weak_constraints=weak} =
diff --git a/engine/uState.mli b/engine/uState.mli
index 23ef84c55d..8855a6bea6 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -100,7 +100,7 @@ val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t ->
    universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
-type rigid = 
+type rigid =
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)