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

2 files changed, 259 insertions, 259 deletions

diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 13da8220f4..4cc32cfb26 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -102,7 +102,7 @@ type sequent =
 let add_one_arrow i f1 f2 m=
   try Fmap.add f1 ((i,f2)::(Fmap.find f1 m)) m with
       Not_found ->
-	Fmap.add f1 [i,f2] m
+        Fmap.add f1 [i,f2] m
 
 type proof =
     Ax of int
@@ -174,7 +174,7 @@ let project = function
 let pop n prf =
   let nprf=
     match prf.dep_it with
-	Pop (i,p) -> Pop (i+n,p)
+        Pop (i,p) -> Pop (i+n,p)
       | p -> Pop(n,p) in
     {prf with dep_it = nprf}
 
@@ -182,71 +182,71 @@ let rec fill stack proof =
   match stack with
       [] -> Complete proof.dep_it
     | slice::super ->
-	if
-	  !pruning &&
-	  List.is_empty slice.proofs_done &&
-	  not (slice.changes_goal && proof.dep_goal) &&
-	  not (Int.Set.exists
-		 (fun i -> Int.Set.mem i proof.dep_hyps)
-		 slice.creates_hyps)
-	then
-	  begin
-	    s_info.pruned_steps<-s_info.pruned_steps+1;
-	    s_info.pruned_branches<- s_info.pruned_branches +
-	    List.length slice.proofs_todo;
-	    let created_here=Int.Set.cardinal slice.creates_hyps in
-	      s_info.pruned_hyps<-s_info.pruned_hyps+
-	      List.fold_left
-		(fun sum dseq -> sum + Int.Set.cardinal dseq.dep_hyps)
-		created_here slice.proofs_todo;
-	    fill super (pop (Int.Set.cardinal slice.creates_hyps) proof)
-	  end
-	else
-	  let dep_hyps=
-	    Int.Set.union slice.needs_hyps
-	      (Int.Set.diff proof.dep_hyps slice.creates_hyps) in
-	  let dep_goal=
-	    slice.needs_goal ||
-	    ((not slice.changes_goal) && proof.dep_goal) in
-	  let proofs_done=
-	    proof.dep_it::slice.proofs_done in
-	    match slice.proofs_todo with
-		[] ->
-		  fill super {dep_it =
-				add_step slice.step (List.rev proofs_done);
-			      dep_goal = dep_goal;
-			      dep_hyps = dep_hyps}
-	      | current::next ->
-		  let nslice=
-		    {proofs_done=proofs_done;
-		     proofs_todo=next;
-		     step=slice.step;
-		     needs_goal=dep_goal;
-		     needs_hyps=dep_hyps;
-		     changes_goal=current.dep_goal;
-		     creates_hyps=current.dep_hyps} in
-		    Incomplete (current.dep_it,nslice::super)
+        if
+          !pruning &&
+          List.is_empty slice.proofs_done &&
+          not (slice.changes_goal && proof.dep_goal) &&
+          not (Int.Set.exists
+                 (fun i -> Int.Set.mem i proof.dep_hyps)
+                 slice.creates_hyps)
+        then
+          begin
+            s_info.pruned_steps<-s_info.pruned_steps+1;
+            s_info.pruned_branches<- s_info.pruned_branches +
+            List.length slice.proofs_todo;
+            let created_here=Int.Set.cardinal slice.creates_hyps in
+              s_info.pruned_hyps<-s_info.pruned_hyps+
+              List.fold_left
+                (fun sum dseq -> sum + Int.Set.cardinal dseq.dep_hyps)
+                created_here slice.proofs_todo;
+            fill super (pop (Int.Set.cardinal slice.creates_hyps) proof)
+          end
+        else
+          let dep_hyps=
+            Int.Set.union slice.needs_hyps
+              (Int.Set.diff proof.dep_hyps slice.creates_hyps) in
+          let dep_goal=
+            slice.needs_goal ||
+            ((not slice.changes_goal) && proof.dep_goal) in
+          let proofs_done=
+            proof.dep_it::slice.proofs_done in
+            match slice.proofs_todo with
+                [] ->
+                  fill super {dep_it =
+                                add_step slice.step (List.rev proofs_done);
+                              dep_goal = dep_goal;
+                              dep_hyps = dep_hyps}
+              | current::next ->
+                  let nslice=
+                    {proofs_done=proofs_done;
+                     proofs_todo=next;
+                     step=slice.step;
+                     needs_goal=dep_goal;
+                     needs_hyps=dep_hyps;
+                     changes_goal=current.dep_goal;
+                     creates_hyps=current.dep_hyps} in
+                    Incomplete (current.dep_it,nslice::super)
 
 let append stack (step,subgoals) =
   s_info.created_steps<-s_info.created_steps+1;
   match subgoals with
       [] ->
-	s_info.branch_successes<-s_info.branch_successes+1;
-	fill stack {dep_it=add_step step.dep_it [];
-		    dep_goal=step.dep_goal;
-		    dep_hyps=step.dep_hyps}
+        s_info.branch_successes<-s_info.branch_successes+1;
+        fill stack {dep_it=add_step step.dep_it [];
+                    dep_goal=step.dep_goal;
+                    dep_hyps=step.dep_hyps}
     | hd :: next ->
-	s_info.created_branches<-
-	s_info.created_branches+List.length next;
-	let slice=
-	  {proofs_done=[];
-	   proofs_todo=next;
-	   step=step.dep_it;
-	   needs_goal=step.dep_goal;
-	   needs_hyps=step.dep_hyps;
-	   changes_goal=hd.dep_goal;
-	   creates_hyps=hd.dep_hyps} in
-	  Incomplete(hd.dep_it,slice::stack)
+        s_info.created_branches<-
+        s_info.created_branches+List.length next;
+        let slice=
+          {proofs_done=[];
+           proofs_todo=next;
+           step=step.dep_it;
+           needs_goal=step.dep_goal;
+           needs_hyps=step.dep_hyps;
+           changes_goal=hd.dep_goal;
+           creates_hyps=hd.dep_hyps} in
+          Incomplete(hd.dep_it,slice::stack)
 
 let embed seq=
   {dep_it=seq;
@@ -266,59 +266,59 @@ let add_hyp seqwd f=
   let cnx,right=
     try
       let l=Fmap.find f seq.right in
-	List.fold_right (fun (i,f0) l0 -> (num,i,f,f0)::l0) l seq.cnx,
-	Fmap.remove f seq.right
+        List.fold_right (fun (i,f0) l0 -> (num,i,f,f0)::l0) l seq.cnx,
+        Fmap.remove f seq.right
     with Not_found -> seq.cnx,seq.right in
   let nseq=
     match f with
-	Bot ->
-	  {seq with
-	     left=left;
-	     right=right;
-	     size=num;
-	     abs=Some num;
-	     cnx=cnx}
+        Bot ->
+          {seq with
+             left=left;
+             right=right;
+             size=num;
+             abs=Some num;
+             cnx=cnx}
       | Atom _ ->
-	  {seq with
-	     size=num;
-	     left=left;
-	     right=right;
-	     cnx=cnx}
+          {seq with
+             size=num;
+             left=left;
+             right=right;
+             cnx=cnx}
       | Conjunct (_,_) | Disjunct (_,_) ->
-	  {seq with
-	     rev_hyps=Int.Map.add num f seq.rev_hyps;
-	     size=num;
-	     left=left;
-	     right=right;
-	     cnx=cnx}
+          {seq with
+             rev_hyps=Int.Map.add num f seq.rev_hyps;
+             size=num;
+             left=left;
+             right=right;
+             cnx=cnx}
       | Arrow (f1,f2) ->
-	  let ncnx,nright=
-	    try
-	      let i = Fmap.find f1 seq.left in
-		(i,num,f1,f2)::cnx,right
-	    with Not_found ->
-	      cnx,(add_one_arrow num f1 f2 right) in
-	    match f1 with
-		Conjunct (_,_) | Disjunct (_,_) ->
-		  {seq with
-		     rev_hyps=Int.Map.add num f seq.rev_hyps;
-		     size=num;
-		     left=left;
-		     right=nright;
-		     cnx=ncnx}
-	      | Arrow(_,_) ->
-		  {seq with
-		     norev_hyps=Int.Map.add num f seq.norev_hyps;
-		     size=num;
-		     left=left;
-		     right=nright;
-		     cnx=ncnx}
-	      | _ ->
-		  {seq with
-		     size=num;
-		     left=left;
-		     right=nright;
-		     cnx=ncnx} in
+          let ncnx,nright=
+            try
+              let i = Fmap.find f1 seq.left in
+                (i,num,f1,f2)::cnx,right
+            with Not_found ->
+              cnx,(add_one_arrow num f1 f2 right) in
+            match f1 with
+                Conjunct (_,_) | Disjunct (_,_) ->
+                  {seq with
+                     rev_hyps=Int.Map.add num f seq.rev_hyps;
+                     size=num;
+                     left=left;
+                     right=nright;
+                     cnx=ncnx}
+              | Arrow(_,_) ->
+                  {seq with
+                     norev_hyps=Int.Map.add num f seq.norev_hyps;
+                     size=num;
+                     left=left;
+                     right=nright;
+                     cnx=ncnx}
+              | _ ->
+                  {seq with
+                     size=num;
+                     left=left;
+                     right=nright;
+                     cnx=ncnx} in
     {seqwd with
        dep_it=nseq;
        dep_hyps=Int.Set.add num seqwd.dep_hyps}
@@ -336,33 +336,33 @@ let choose m=
 let search_or seq=
   match seq.gl with
       Disjunct (f1,f2) ->
-	[{dep_it = SI_Or_l;
-	  dep_goal = true;
-	  dep_hyps = Int.Set.empty},
-	 [change_goal (embed seq) f1];
-	 {dep_it = SI_Or_r;
-	  dep_goal = true;
-	  dep_hyps = Int.Set.empty},
-	 [change_goal (embed seq) f2]]
+        [{dep_it = SI_Or_l;
+          dep_goal = true;
+          dep_hyps = Int.Set.empty},
+         [change_goal (embed seq) f1];
+         {dep_it = SI_Or_r;
+          dep_goal = true;
+          dep_hyps = Int.Set.empty},
+         [change_goal (embed seq) f2]]
     | _ -> []
 
 let search_norev seq=
   let goals=ref (search_or seq) in
   let add_one i f=
     match f with
-	Arrow (Arrow (f1,f2),f3) ->
-	  let nseq =
-	    {seq with norev_hyps=Int.Map.remove i seq.norev_hyps} in
-	    goals:=
-	      ({dep_it=SD_Arrow(i);
-		dep_goal=false;
-		dep_hyps=Int.Set.singleton i},
-	       [add_hyp
-		  (add_hyp
-		     (change_goal (embed nseq) f2)
-		     (Arrow(f2,f3)))
-		  f1;
-		add_hyp (embed nseq) f3]):: !goals
+        Arrow (Arrow (f1,f2),f3) ->
+          let nseq =
+            {seq with norev_hyps=Int.Map.remove i seq.norev_hyps} in
+            goals:=
+              ({dep_it=SD_Arrow(i);
+                dep_goal=false;
+                dep_hyps=Int.Set.singleton i},
+               [add_hyp
+                  (add_hyp
+                     (change_goal (embed nseq) f2)
+                     (Arrow(f2,f3)))
+                  f1;
+                add_hyp (embed nseq) f3]):: !goals
       | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen.") in
     Int.Map.iter add_one seq.norev_hyps;
     List.rev !goals
@@ -376,76 +376,76 @@ let search_in_rev_hyps seq=
        dep_hyps=Int.Set.singleton i} in
     let nseq={seq with rev_hyps=Int.Map.remove i seq.rev_hyps} in
       match f with
-	  Conjunct (f1,f2) ->
-	    [make_step (SE_And(i)),
-	     [add_hyp (add_hyp (embed nseq) f1) f2]]
-	| Disjunct (f1,f2) ->
-	    [make_step (SE_Or(i)),
-	     [add_hyp (embed nseq) f1;add_hyp (embed nseq) f2]]
-	| Arrow (Conjunct (f1,f2),f0) ->
-	    [make_step (SD_And(i)),
-	     [add_hyp (embed nseq) (Arrow (f1,Arrow (f2,f0)))]]
-	| Arrow (Disjunct (f1,f2),f0) ->
-	    [make_step (SD_Or(i)),
-	     [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]]
-	| _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen.")
+          Conjunct (f1,f2) ->
+            [make_step (SE_And(i)),
+             [add_hyp (add_hyp (embed nseq) f1) f2]]
+        | Disjunct (f1,f2) ->
+            [make_step (SE_Or(i)),
+             [add_hyp (embed nseq) f1;add_hyp (embed nseq) f2]]
+        | Arrow (Conjunct (f1,f2),f0) ->
+            [make_step (SD_And(i)),
+             [add_hyp (embed nseq) (Arrow (f1,Arrow (f2,f0)))]]
+        | Arrow (Disjunct (f1,f2),f0) ->
+            [make_step (SD_Or(i)),
+             [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]]
+        | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen.")
   with
       Not_found -> search_norev seq
 
 let search_rev seq=
   match seq.cnx with
       (i,j,f1,f2)::next ->
-	let nseq=
-	  match f1 with
-	      Conjunct (_,_) | Disjunct (_,_) ->
-		{seq with cnx=next;
-		   rev_hyps=Int.Map.remove j seq.rev_hyps}
-	    | Arrow (_,_) ->
-		{seq with cnx=next;
-		   norev_hyps=Int.Map.remove j seq.norev_hyps}
-	    | _ ->
-		{seq with cnx=next} in
-	  [{dep_it=SE_Arrow(i,j);
-	    dep_goal=false;
-	    dep_hyps=Int.Set.add i (Int.Set.singleton j)},
-	   [add_hyp (embed nseq) f2]]
+        let nseq=
+          match f1 with
+              Conjunct (_,_) | Disjunct (_,_) ->
+                {seq with cnx=next;
+                   rev_hyps=Int.Map.remove j seq.rev_hyps}
+            | Arrow (_,_) ->
+                {seq with cnx=next;
+                   norev_hyps=Int.Map.remove j seq.norev_hyps}
+            | _ ->
+                {seq with cnx=next} in
+          [{dep_it=SE_Arrow(i,j);
+            dep_goal=false;
+            dep_hyps=Int.Set.add i (Int.Set.singleton j)},
+           [add_hyp (embed nseq) f2]]
     | [] ->
-	match seq.gl with
-	    Arrow (f1,f2) ->
-	      [{dep_it=SI_Arrow;
-		dep_goal=true;
-		dep_hyps=Int.Set.empty},
-	       [add_hyp (change_goal (embed seq) f2) f1]]
-	  | Conjunct (f1,f2) ->
-	      [{dep_it=SI_And;
-		dep_goal=true;
-		dep_hyps=Int.Set.empty},[change_goal (embed seq) f1;
-					change_goal (embed seq) f2]]
-	  | _ -> search_in_rev_hyps seq
+        match seq.gl with
+            Arrow (f1,f2) ->
+              [{dep_it=SI_Arrow;
+                dep_goal=true;
+                dep_hyps=Int.Set.empty},
+               [add_hyp (change_goal (embed seq) f2) f1]]
+          | Conjunct (f1,f2) ->
+              [{dep_it=SI_And;
+                dep_goal=true;
+                dep_hyps=Int.Set.empty},[change_goal (embed seq) f1;
+                                        change_goal (embed seq) f2]]
+          | _ -> search_in_rev_hyps seq
 
 let search_all seq=
   match seq.abs with
       Some i ->
-	[{dep_it=SE_False (i);
-	  dep_goal=false;
-	  dep_hyps=Int.Set.singleton i},[]]
+        [{dep_it=SE_False (i);
+          dep_goal=false;
+          dep_hyps=Int.Set.singleton i},[]]
     | None ->
-	try
-	  let ax = Fmap.find seq.gl seq.left in
-	    [{dep_it=SAx (ax);
-	      dep_goal=true;
-	      dep_hyps=Int.Set.singleton ax},[]]
-	with Not_found -> search_rev seq
+        try
+          let ax = Fmap.find seq.gl seq.left in
+            [{dep_it=SAx (ax);
+              dep_goal=true;
+              dep_hyps=Int.Set.singleton ax},[]]
+        with Not_found -> search_rev seq
 
 let bare_sequent = embed
-		     {rev_hyps=Int.Map.empty;
-		      norev_hyps=Int.Map.empty;
-		      size=0;
-		      left=Fmap.empty;
-		      right=Fmap.empty;
-		      cnx=[];
-		      abs=None;
-		      gl=Bot}
+                     {rev_hyps=Int.Map.empty;
+                      norev_hyps=Int.Map.empty;
+                      size=0;
+                      left=Fmap.empty;
+                      right=Fmap.empty;
+                      cnx=[];
+                      abs=None;
+                      gl=Bot}
 
 let init_state hyps gl=
   let init = change_goal bare_sequent gl in
@@ -461,11 +461,11 @@ let branching = function
       Control.check_for_interrupt ();
       let successors = search_all seq in
       let _ =
-	match successors with
-	    [] -> s_info.branch_failures<-s_info.branch_failures+1
-	  | _::next ->
-	      s_info.nd_branching<-s_info.nd_branching+List.length next in
-	List.map (append stack) successors
+        match successors with
+            [] -> s_info.branch_failures<-s_info.branch_failures+1
+          | _::next ->
+              s_info.nd_branching<-s_info.nd_branching+List.length next in
+        List.map (append stack) successors
   | Complete prf -> anomaly (Pp.str "already succeeded.")
 
 open Pp
@@ -492,7 +492,7 @@ let pr_form f = pp_form f
 let pp_intmap map =
   let pp=ref (str "") in
    Int.Map.iter (fun i obj -> pp:= (!pp ++
-		pp_form obj ++ cut ())) map;
+                pp_form obj ++ cut ())) map;
     str "{ " ++ v 0 (!pp) ++ str " }"
 
 let pp_list pp_obj l=
@@ -503,20 +503,20 @@ let pp=ref (str "") in
 let pp_mapint map =
   let pp=ref (str "") in
    Fmap.iter (fun obj l -> pp:= (!pp ++
-		pp_form obj ++ str " => " ++
-				 pp_list (fun (i,f) -> pp_form f) l ++
-				 cut ()) ) map;
+                pp_form obj ++ str " => " ++
+                                 pp_list (fun (i,f) -> pp_form f) l ++
+                                 cut ()) ) map;
     str "{ " ++ hv 0 (!pp ++ str " }")
 
 let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2
 
 let pp_gl gl= cut () ++
   str "{ " ++ hv 0 (
-	      begin
-		match gl.abs with
-		    None -> str ""
-		  | Some i -> str "ABSURD" ++ cut ()
-	      end ++
+              begin
+                match gl.abs with
+                    None -> str ""
+                  | Some i -> str "ABSURD" ++ cut ()
+              end ++
   str "rev   =" ++ pp_intmap gl.rev_hyps ++ cut () ++
   str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++
   str "arrows=" ++ pp_mapint gl.right ++ cut () ++
@@ -531,31 +531,31 @@ let pp =
 let pp_info () =
   let count_info =
     if !pruning then
-	str "Proof steps : " ++
-	int s_info.created_steps ++ str " created / " ++
-	int s_info.pruned_steps ++ str " pruned" ++ fnl () ++
-	str "Proof branches : " ++
-	int s_info.created_branches ++ str " created / " ++
-	int s_info.pruned_branches ++ str " pruned" ++ fnl () ++
-	str "Hypotheses : " ++
-	int s_info.created_hyps ++ str " created / " ++
-	int s_info.pruned_hyps ++ str " pruned" ++ fnl ()
+        str "Proof steps : " ++
+        int s_info.created_steps ++ str " created / " ++
+        int s_info.pruned_steps ++ str " pruned" ++ fnl () ++
+        str "Proof branches : " ++
+        int s_info.created_branches ++ str " created / " ++
+        int s_info.pruned_branches ++ str " pruned" ++ fnl () ++
+        str "Hypotheses : " ++
+        int s_info.created_hyps ++ str " created / " ++
+        int s_info.pruned_hyps ++ str " pruned" ++ fnl ()
     else
-	str "Pruning is off" ++ fnl () ++
-	str "Proof steps : " ++
-	int s_info.created_steps ++ str " created" ++ fnl () ++
-	str "Proof branches : " ++
-	int s_info.created_branches ++ str " created" ++ fnl () ++
-	str "Hypotheses : " ++
-	int s_info.created_hyps ++ str " created" ++ fnl () in
+        str "Pruning is off" ++ fnl () ++
+        str "Proof steps : " ++
+        int s_info.created_steps ++ str " created" ++ fnl () ++
+        str "Proof branches : " ++
+        int s_info.created_branches ++ str " created" ++ fnl () ++
+        str "Hypotheses : " ++
+        int s_info.created_hyps ++ str " created" ++ fnl () in
     Feedback.msg_info
       ( str "Proof-search statistics :" ++ fnl () ++
-	count_info ++
-	str "Branch ends: " ++
-	int s_info.branch_successes ++ str " successes / " ++
-	int s_info.branch_failures ++ str " failures" ++ fnl () ++
-	str "Non-deterministic choices : " ++
-	int s_info.nd_branching ++ str " branches")
+        count_info ++
+        str "Branch ends: " ++
+        int s_info.branch_successes ++ str " successes / " ++
+        int s_info.branch_failures ++ str " failures" ++ fnl () ++
+        str "Non-deterministic choices : " ++
+        int s_info.nd_branching ++ str " branches")
 
 
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index df27c9c9d7..0c155c9d0a 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -156,9 +156,9 @@ let rec decal k = function
     [] -> k
   | (start,delta)::rest ->
       if k>start then
-	k - delta
+        k - delta
       else
-	decal k rest
+        decal k rest
 
 let add_pop size d pops=
   match pops with
@@ -168,57 +168,57 @@ let add_pop size d pops=
 let rec build_proof pops size =
   function
       Ax i ->
-	mkApp (force step_count l_Ax,
-	       [|build_pos (decal i pops)|])
+        mkApp (force step_count l_Ax,
+               [|build_pos (decal i pops)|])
       | I_Arrow p ->
-	  mkApp (force step_count l_I_Arrow,
-		 [|build_proof pops (size + 1) p|])
+          mkApp (force step_count l_I_Arrow,
+                 [|build_proof pops (size + 1) p|])
       | E_Arrow(i,j,p) ->
-	  mkApp (force step_count l_E_Arrow,
-		 [|build_pos (decal i pops);
-		   build_pos (decal j pops);
-		   build_proof pops (size + 1) p|])
+          mkApp (force step_count l_E_Arrow,
+                 [|build_pos (decal i pops);
+                   build_pos (decal j pops);
+                   build_proof pops (size + 1) p|])
       | D_Arrow(i,p1,p2) ->
-	  mkApp (force step_count l_D_Arrow,
-		 [|build_pos (decal i pops);
-		   build_proof pops (size + 2) p1;
-		   build_proof pops (size + 1) p2|])
+          mkApp (force step_count l_D_Arrow,
+                 [|build_pos (decal i pops);
+                   build_proof pops (size + 2) p1;
+                   build_proof pops (size + 1) p2|])
       | E_False i ->
-	  mkApp (force step_count l_E_False,
-		 [|build_pos (decal i pops)|])
+          mkApp (force step_count l_E_False,
+                 [|build_pos (decal i pops)|])
       | I_And(p1,p2) ->
-	  mkApp (force step_count l_I_And,
-		 [|build_proof pops size p1;
-		   build_proof pops size p2|])
+          mkApp (force step_count l_I_And,
+                 [|build_proof pops size p1;
+                   build_proof pops size p2|])
       | E_And(i,p) ->
-	  mkApp (force step_count l_E_And,
-		 [|build_pos (decal i pops);
-		   build_proof pops (size + 2) p|])
+          mkApp (force step_count l_E_And,
+                 [|build_pos (decal i pops);
+                   build_proof pops (size + 2) p|])
       | D_And(i,p) ->
-	  mkApp (force step_count l_D_And,
-		 [|build_pos (decal i pops);
-		   build_proof pops (size + 1) p|])
+          mkApp (force step_count l_D_And,
+                 [|build_pos (decal i pops);
+                   build_proof pops (size + 1) p|])
       | I_Or_l(p) ->
-	  mkApp (force step_count l_I_Or_l,
-		 [|build_proof pops size p|])
+          mkApp (force step_count l_I_Or_l,
+                 [|build_proof pops size p|])
       | I_Or_r(p) ->
-	  mkApp (force step_count l_I_Or_r,
-		 [|build_proof pops size p|])
+          mkApp (force step_count l_I_Or_r,
+                 [|build_proof pops size p|])
       | E_Or(i,p1,p2) ->
-	  mkApp (force step_count l_E_Or,
-		 [|build_pos (decal i pops);
-		   build_proof pops (size + 1) p1;
-		   build_proof pops (size + 1) p2|])
+          mkApp (force step_count l_E_Or,
+                 [|build_pos (decal i pops);
+                   build_proof pops (size + 1) p1;
+                   build_proof pops (size + 1) p2|])
       | D_Or(i,p) ->
-	  mkApp (force step_count l_D_Or,
-		 [|build_pos (decal i pops);
-		   build_proof pops (size + 2) p|])
+          mkApp (force step_count l_D_Or,
+                 [|build_pos (decal i pops);
+                   build_proof pops (size + 2) p|])
       | Pop(d,p) ->
-	  build_proof (add_pop size d pops) size p
+          build_proof (add_pop size d pops) size p
 
 let build_env gamma=
   List.fold_right (fun (p,_) e ->
-		     mkApp(force node_count l_push,[|mkProp;p;e|]))
+                     mkApp(force node_count l_push,[|mkProp;p;e|]))
     gamma.env (mkApp (force node_count l_empty,[|mkProp|]))
 
 open Goptions