From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 17 Sep 2009 15:58:14 +0000
Subject: Delete trailing whitespaces in all *.{v,ml*} files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/firstorder/ground.ml | 58 ++++++++++++++++++++++----------------------
 1 file changed, 29 insertions(+), 29 deletions(-)

(limited to 'plugins/firstorder/ground.ml')

diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index a8d5fc2ef..8a0f02d27 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -19,10 +19,10 @@ open Tacticals
 open Libnames
 
 (*
-let old_search=ref !Auto.searchtable 
+let old_search=ref !Auto.searchtable
 
-(* I use this solution as a means to know whether hints have changed, 
-but this prevents the GC from collecting the previous table, 
+(* I use this solution as a means to know whether hints have changed,
+but this prevents the GC from collecting the previous table,
 resulting in some limited space wasting*)
 
 let update_flags ()=
@@ -30,7 +30,7 @@ let update_flags ()=
     begin
       old_search:=!Auto.searchtable;
       let predref=ref Names.KNpred.empty in
-      let f p_a_t = 
+      let f p_a_t =
 	match p_a_t.Auto.code with
 	    Auto.Unfold_nth (ConstRef kn)->
 	      predref:=Names.KNpred.add kn !predref
@@ -39,7 +39,7 @@ let update_flags ()=
       let h _ hdb=Auto.Hint_db.iter g hdb in
 	Util.Stringmap.iter h !Auto.searchtable;
 	red_flags:=
-	Closure.RedFlags.red_add_transparent 
+	Closure.RedFlags.red_add_transparent
 	  Closure.betaiotazeta (Names.Idpred.full,!predref)
     end
 *)
@@ -53,8 +53,8 @@ let update_flags ()=
     with Invalid_argument "destConst"-> () in
     List.iter f (Classops.coercions ());
     red_flags:=
-    Closure.RedFlags.red_add_transparent 
-      Closure.betaiotazeta 
+    Closure.RedFlags.red_add_transparent
+      Closure.betaiotazeta
       (Names.Idpred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
@@ -64,10 +64,10 @@ let ground_tac solver startseq gl=
     then Pp.msgnl (Printer.pr_goal (sig_it gl));
     tclORELSE (axiom_tac seq.gl seq)
       begin
-	try      
-	  let (hd,seq1)=take_formula seq  
+	try
+	  let (hd,seq1)=take_formula seq
 	  and re_add s=re_add_formula_list skipped s in
-	  let continue=toptac [] 
+	  let continue=toptac []
 	  and backtrack gl=toptac (hd::skipped) seq1 gl in
 	    match hd.pat with
 		Right rpat->
@@ -77,7 +77,7 @@ let ground_tac solver startseq gl=
 			  and_tac backtrack continue (re_add seq1)
 		      | Rforall->
 			  let backtrack1=
-			    if !qflag then 
+			    if !qflag then
 			      tclFAIL 0 (Pp.str "reversible in 1st order mode")
 			    else
 			      backtrack in
@@ -86,12 +86,12 @@ let ground_tac solver startseq gl=
 			  arrow_tac backtrack continue (re_add seq1)
 		      | Ror->
 			  or_tac  backtrack continue (re_add seq1)
-		      | Rfalse->backtrack 
+		      | Rfalse->backtrack
 		      | Rexists(i,dom,triv)->
 			  let (lfp,seq2)=collect_quantified seq in
 			  let backtrack2=toptac (lfp@skipped) seq2 in
-			    if  !qflag && seq.depth>0 then 
-			      quantified_tac lfp backtrack2 
+			    if  !qflag && seq.depth>0 then
+			      quantified_tac lfp backtrack2
 				continue (re_add seq)
 			    else
 			      backtrack2 (* need special backtracking *)
@@ -102,21 +102,21 @@ let ground_tac solver startseq gl=
 			Lfalse->
 			  left_false_tac hd.id
 		      | Land ind->
-			  left_and_tac ind backtrack 
+			  left_and_tac ind backtrack
 			  hd.id continue (re_add seq1)
 		      | Lor ind->
-			  left_or_tac ind backtrack 
+			  left_or_tac ind backtrack
 			  hd.id continue (re_add seq1)
 		      | Lforall (_,_,_)->
 			  let (lfp,seq2)=collect_quantified seq in
 			  let backtrack2=toptac (lfp@skipped) seq2 in
-			    if  !qflag && seq.depth>0 then 
-			      quantified_tac lfp backtrack2 
+			    if  !qflag && seq.depth>0 then
+			      quantified_tac lfp backtrack2
 				continue (re_add seq)
 			    else
 			      backtrack2 (* need special backtracking *)
   		      | Lexists ind ->
-			  if !qflag then 
+			  if !qflag then
 			    left_exists_tac ind backtrack hd.id
 			      continue (re_add seq1)
 			  else backtrack
@@ -124,14 +124,14 @@ let ground_tac solver startseq gl=
 			  let la_tac=
 			    begin
 			      match lap with
-				  LLatom -> backtrack 
-				| LLand (ind,largs) | LLor(ind,largs) 
+				  LLatom -> backtrack
+				| LLand (ind,largs) | LLor(ind,largs)
 				| LLfalse (ind,largs)->
-				    (ll_ind_tac ind largs backtrack 
-				       hd.id continue (re_add seq1)) 
-				| LLforall p ->	      
-				    if seq.depth>0 && !qflag then 
-				      (ll_forall_tac p backtrack 
+				    (ll_ind_tac ind largs backtrack
+				       hd.id continue (re_add seq1))
+				| LLforall p ->
+				    if seq.depth>0 && !qflag then
+				      (ll_forall_tac p backtrack
 					 hd.id continue (re_add seq1))
 				    else backtrack
 				| LLexists (ind,l) ->
@@ -140,13 +140,13 @@ let ground_tac solver startseq gl=
 					hd.id continue (re_add seq1)
 				    else
 				      backtrack
-				| LLarrow (a,b,c) ->	      
+				| LLarrow (a,b,c) ->
 				    (ll_arrow_tac a b c backtrack
 				       hd.id continue (re_add seq1))
-			    end in			 
+			    end in
 			    ll_atom_tac typ la_tac hd.id continue (re_add seq1)
 		  end
 	    with Heap.EmptyHeap->solver
       end gl in
     wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
-      
+
-- 
cgit v1.2.3