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, 26 insertions, 26 deletions

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e9aa692b6..87d646ab8 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,10 +1,10 @@
 open Names
 open Pp
 
-(* 
-   The mk_?_id function build different name w.r.t. a function 
-   Each of their use is justified in the code 
-*) 
+(*
+   The mk_?_id function build different name w.r.t. a function
+   Each of their use is justified in the code
+*)
 val mk_rel_id : identifier -> identifier
 val mk_correct_id : identifier -> identifier
 val mk_complete_id : identifier -> identifier
@@ -16,8 +16,8 @@ val msgnl : std_ppcmds -> unit
 val invalid_argument : string -> 'a
 
 val fresh_id : identifier list -> string -> identifier
-val fresh_name : identifier list -> string -> name 
-val get_name : identifier list -> ?default:string -> name -> name 
+val fresh_name : identifier list -> string -> name
+val get_name : identifier list -> ?default:string -> name -> name
 
 val array_get_start : 'a array -> 'a array
 
@@ -46,11 +46,11 @@ val eq : Term.constr Lazy.t
 val refl_equal : Term.constr Lazy.t
 val const_of_id: identifier -> constant
 val jmeq : unit -> Term.constr
-val jmeq_refl : unit -> Term.constr 
+val jmeq_refl : unit -> Term.constr
+
+(* [save_named] is a copy of [Command.save_named] but uses
+   [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast]
 
-(* [save_named] is a copy of [Command.save_named] but uses 
-   [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast] 
-   
 
 
    DON'T USE IT if you cannot ensure that there is no VMcast in the proof
@@ -59,32 +59,32 @@ val jmeq_refl : unit -> Term.constr
 
 (* val nf_betaiotazeta : Reductionops.reduction_function *)
 
-val new_save_named : bool -> unit 
+val new_save_named : bool -> unit
 
-val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind -> 
-  Tacexpr.declaration_hook -> unit 
+val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
+  Tacexpr.declaration_hook -> unit
 
-(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and 
-   abort the proof 
+(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
+   abort the proof
 *)
-val get_proof_clean : bool ->     
+val get_proof_clean : bool ->
   Names.identifier *
     (Entries.definition_entry * Decl_kinds.goal_kind *
        Tacexpr.declaration_hook)
-    
 
 
-(* [with_full_print f a] applies [f] to [a] in full printing environment 
-   
-   This function preserves the print settings 
+
+(* [with_full_print f a] applies [f] to [a] in full printing environment
+
+   This function preserves the print settings
 *)
 val with_full_print : ('a -> 'b) -> 'a -> 'b
 
 
 (*****************)
 
-type function_info = 
-    { 
+type function_info =
+    {
       function_constant : constant;
       graph_ind : inductive;
       equation_lemma : constant option;
@@ -101,10 +101,10 @@ val find_Function_of_graph : inductive -> function_info
 (* WARNING: To be used just after the graph definition !!! *)
 val add_Function : bool -> constant -> unit
 
-val update_Function : function_info -> unit 
+val update_Function : function_info -> unit
 
 
-(** debugging *) 
+(** debugging *)
 val pr_info : function_info -> Pp.std_ppcmds
 val pr_table : unit -> Pp.std_ppcmds
 
@@ -113,8 +113,8 @@ val pr_table : unit -> Pp.std_ppcmds
 val do_observe : unit -> bool
 
 (* To localize pb *)
-exception Building_graph of exn 
+exception Building_graph of exn
 exception Defining_principle of exn
-exception ToShow of exn 
+exception ToShow of exn
 
 val is_strict_tcc : unit -> bool