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/formula.mli | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'plugins/firstorder/formula.mli')

diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 9e9d1e122..2e89ddb06 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -16,10 +16,10 @@ val qflag : bool ref
 
 val red_flags: Closure.RedFlags.reds ref
 
-val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 
+val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
   'a -> 'a -> 'b -> 'b -> int
-  
-val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> 
+
+val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) ->
   'a -> 'a -> 'b -> 'b -> 'c ->'c -> int
 
 type ('a,'b) sum = Left of 'a | Right of 'b
@@ -28,7 +28,7 @@ type counter = bool -> metavariable
 
 val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
 
-val ind_hyps : int -> inductive -> constr list -> 
+val ind_hyps : int -> inductive -> constr list ->
   Proof_type.goal Tacmach.sigma -> rel_context array
 
 type atoms = {positive:constr list;negative:constr list}
@@ -36,18 +36,18 @@ type atoms = {positive:constr list;negative:constr list}
 type side = Hyp | Concl | Hint
 
 val dummy_id: global_reference
-			
-val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> 
+
+val build_atoms : Proof_type.goal Tacmach.sigma -> counter ->
   side -> constr -> bool * atoms
 
 type right_pattern =
     Rarrow
   | Rand
-  | Ror 
+  | Ror
   | Rfalse
   | Rforall
   | Rexists of metavariable*constr*bool
-    
+
 type left_arrow_pattern=
     LLatom
   | LLfalse of inductive*constr list
@@ -58,20 +58,20 @@ type left_arrow_pattern=
   | LLarrow of constr*constr*constr
 
 type left_pattern=
-    Lfalse    
+    Lfalse
   | Land of inductive
-  | Lor of inductive 
+  | Lor of inductive
   | Lforall of metavariable*constr*bool
   | Lexists of inductive
   | LA of constr*left_arrow_pattern
-      
+
 type t={id: global_reference;
 	constr: constr;
 	pat: (left_pattern,right_pattern) sum;
 	atoms: atoms}
-    
+
 (*exception Is_atom of constr*)
 
-val build_formula : side -> global_reference -> types -> 
+val build_formula : side -> global_reference -> types ->
   Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum
 
-- 
cgit v1.2.3