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

1 files changed, 20 insertions, 20 deletions

diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3f5411e00..001755b1e 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -42,8 +42,8 @@ open Coqlib
    is an inductive but non-recursive type, a general conjuction, a
    general disjunction, or a type with no constructors.
 
-   They are more general than matching with [or_term], [and_term], etc, 
-   since they do not depend on the name of the type. Hence, they 
+   They are more general than matching with [or_term], [and_term], etc,
+   since they do not depend on the name of the type. Hence, they
    also work on ad-hoc disjunctions introduced by the user.
    (Eduardo, 6/8/97). *)
 
@@ -51,49 +51,49 @@ type 'a matching_function = constr -> 'a option
 type testing_function = constr -> bool
 
 val match_with_non_recursive_type : (constr * constr list) matching_function
-val is_non_recursive_type         : testing_function 
+val is_non_recursive_type         : testing_function
 
 (* Non recursive type with no indices and exactly one argument for each
    constructor; canonical definition of n-ary disjunction if strict *)
 val match_with_disjunction : ?strict:bool -> (constr * constr list) matching_function
-val is_disjunction         : ?strict:bool -> testing_function 
+val is_disjunction         : ?strict:bool -> testing_function
 
 (* Non recursive tuple (one constructor and no indices) with no inner
    dependencies; canonical definition of n-ary conjunction if strict *)
 val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function
-val is_conjunction         : ?strict:bool -> testing_function 
+val is_conjunction         : ?strict:bool -> testing_function
 
 (* Non recursive tuple, possibly with inner dependencies *)
 val match_with_record      : (constr * constr list) matching_function
-val is_record              : testing_function 
+val is_record              : testing_function
 
 (* Like record but supports and tells if recursive (e.g. Acc) *)
 val match_with_tuple       : (constr * constr list * bool) matching_function
-val is_tuple               : testing_function 
+val is_tuple               : testing_function
 
 (* No constructor, possibly with indices *)
 val match_with_empty_type  : constr matching_function
-val is_empty_type          : testing_function 
+val is_empty_type          : testing_function
 
 (* type with only one constructor and no arguments, possibly with indices *)
 val match_with_unit_or_eq_type : constr matching_function
-val is_unit_or_eq_type     : testing_function 
+val is_unit_or_eq_type     : testing_function
 
 (* type with only one constructor and no arguments, no indices *)
-val is_unit_type           : testing_function 
+val is_unit_type           : testing_function
 
 (* type with only one constructor, no arguments and at least one dependency *)
 val match_with_equality_type : (constr * constr list) matching_function
 val is_equality_type       : testing_function
 
 val match_with_nottype     : (constr * constr) matching_function
-val is_nottype             : testing_function 
+val is_nottype             : testing_function
 
 val match_with_forall_term    : (name * constr * constr) matching_function
-val is_forall_term            : testing_function 
+val is_forall_term            : testing_function
 
 val match_with_imp_term    : (constr * constr) matching_function
-val is_imp_term            : testing_function 
+val is_imp_term            : testing_function
 
 (* I added these functions to test whether a type contains dependent
   products or not, and if an inductive has constructors with dependent types
@@ -103,11 +103,11 @@ val is_imp_term            : testing_function
 val has_nodep_prod_after   : int -> testing_function
 val has_nodep_prod         : testing_function
 
-val match_with_nodep_ind   : (constr * constr list * int) matching_function  
-val is_nodep_ind           : testing_function 
+val match_with_nodep_ind   : (constr * constr list * int) matching_function
+val is_nodep_ind           : testing_function
 
-val match_with_sigma_type   : (constr * constr list) matching_function	  
-val is_sigma_type           : testing_function 
+val match_with_sigma_type   : (constr * constr list) matching_function
+val is_sigma_type           : testing_function
 
 (* Recongnize inductive relation defined by reflexivity *)
 
@@ -125,11 +125,11 @@ val match_with_equation:
 
 (* Match terms [eq A t u], [identity A t u] or [JMeq A t A u] *)
 (* Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
-val find_eq_data_decompose : Proof_type.goal sigma -> constr -> 
+val find_eq_data_decompose : Proof_type.goal sigma -> constr ->
       coq_eq_data * (types * constr * constr)
 
 (* Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : Proof_type.goal sigma -> constr -> 
+val find_this_eq_data_decompose : Proof_type.goal sigma -> constr ->
       coq_eq_data * (types * constr * constr)
 
 (* A variant that returns more informative structure on the equality found *)
@@ -137,7 +137,7 @@ val find_eq_data : constr -> coq_eq_data * equation_kind
 
 (* Match a term of the form [(existT A P t p)] *)
 (* Returns associated lemmas and [A,P,t,p] *)
-val find_sigma_data_decompose : constr -> 
+val find_sigma_data_decompose : constr ->
   coq_sigma_data * (constr * constr * constr * constr)
 
 (* Match a term of the form [{x:A|P}], returns [A] and [P] *)