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
```
---
 engine/evd.ml | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'engine/evd.ml')

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
 
-- 
cgit v1.2.3