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

6 files changed, 61 insertions, 61 deletions

diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml
index 2153ef47c0..4eb135d83c 100644
--- a/dev/ocamlweb-doc/ast.ml
+++ b/dev/ocamlweb-doc/ast.ml
@@ -22,7 +22,7 @@ type constr_ast =
       (string * binder list * constr_ast * string option * constr_ast) list *
       string
 | Match of case_item list * constr_ast option *
-           (pattern list * constr_ast) list 
+           (pattern list * constr_ast) list
 
 and red_fun = Simpl
 
@@ -34,7 +34,7 @@ and fix_kind = Fix | CoFix
 
 and case_item = constr_ast * (string option * constr_ast option)
 
-and pattern = 
+and pattern =
   PatAs of pattern * string
 | PatType of pattern * constr_ast
 | PatConstr of string * pattern list
diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll
index 617163e7e7..059526d9bf 100644
--- a/dev/ocamlweb-doc/lex.mll
+++ b/dev/ocamlweb-doc/lex.mll
@@ -7,7 +7,7 @@
 
  let comment_depth = ref 0
  let print s = output_string !chan_out s
- 
+
  exception Fin_fichier
 
 }
@@ -77,5 +77,5 @@ and comment = parse
   | "(*" (*"*)"*)  { incr comment_depth; comment lexbuf }
   | (*"(*"*) "*)"
       { decr comment_depth; if !comment_depth > 0 then comment lexbuf }
-  | eof   { raise Fin_fichier } 
+  | eof   { raise Fin_fichier }
   | _     { comment lexbuf }
diff --git a/dev/ocamlweb-doc/parse.ml b/dev/ocamlweb-doc/parse.ml
index e537b1f2f4..b145fffda6 100644
--- a/dev/ocamlweb-doc/parse.ml
+++ b/dev/ocamlweb-doc/parse.ml
@@ -82,7 +82,7 @@ let rec str_stack = function
   | Term (t,s) -> str_stack s ^ " (" ^ str_ast t ^ ")"
   | Oper(ops,lop,t,s) ->
       str_stack (Term(t,s)) ^ " " ^ lop ^ " " ^
-      String.concat " " (List.rev ops) 
+      String.concat " " (List.rev ops)
 
 let pps s = prerr_endline (str_stack s)
 let err s stk = failwith (s^": "^str_stack stk)
diff --git a/dev/printers.mllib b/dev/printers.mllib
index f4b3d7f6c3..107b2904aa 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -6,17 +6,17 @@ Compat
 Flags
 Util
 Bigint
-Hashcons 
+Hashcons
 Dyn
 System
-Envars 
-Bstack 
+Envars
+Bstack
 Edit
-Gset 
+Gset
 Gmap
-Tlm 
+Tlm
 Gmapl
-Profile 
+Profile
 Explore
 Predicate
 Rtree
@@ -107,7 +107,7 @@ Proof_type
 Logic
 Refiner
 Evar_refiner
-Pfedit 
+Pfedit
 Tactic_debug
 Decl_mode
 Ppconstr
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b35d5d4899..d5ebde7cb0 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -71,11 +71,11 @@ let ppidset l = pp (prset pr_id (Idset.elements l))
 
 let pP s = pp (hov 0 s)
 
-let safe_pr_global = function 
+let safe_pr_global = function
   | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")")
-  | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
+  | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++
 			  int i ++ str ")")
-  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
+  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++
 				      int i ++ str "," ++ int j ++ str ")")
   | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
 
@@ -135,7 +135,7 @@ let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
 let cnt = ref 0
 
-let cast_kind_display k = 
+let cast_kind_display k =
   match k with
   | VMcast -> "VMcast"
   | DEFAULTcast -> "DEFAULTcast"
@@ -146,7 +146,7 @@ let constr_display csr =
   | Meta n -> "Meta("^(string_of_int n)^")"
   | Var id -> "Var("^(string_of_id id)^")"
   | Sort s -> "Sort("^(sort_display s)^")"
-  | Cast (c,k, t) -> 
+  | Cast (c,k, t) ->
       "Cast("^(term_display c)^","^(cast_kind_display k)^","^(term_display t)^")"
   | Prod (na,t,c) ->
       "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
@@ -213,25 +213,25 @@ let print_pure_constr csr =
       print_string "::"; (term_display t); print_string ")"; close_box()
   | Prod (Name(id),t,c) ->
       open_hovbox 1;
-      print_string"("; print_string (string_of_id id); 
-      print_string ":"; box_display t; 
-      print_string ")"; print_cut(); 
+      print_string"("; print_string (string_of_id id);
+      print_string ":"; box_display t;
+      print_string ")"; print_cut();
       box_display c; close_box()
   | Prod (Anonymous,t,c) ->
       print_string"("; box_display t; print_cut(); print_string "->";
-      box_display c; print_string ")"; 
+      box_display c; print_string ")";
   | Lambda (na,t,c) ->
       print_string "["; name_display na;
       print_string ":"; box_display t; print_string "]";
-      print_cut(); box_display c; 
+      print_cut(); box_display c;
   | LetIn (na,b,t,c) ->
-      print_string "["; name_display na; print_string "="; 
+      print_string "["; name_display na; print_string "=";
       box_display b; print_cut();
       print_string ":"; box_display t; print_string "]";
-      print_cut(); box_display c; 
-  | App (c,l) -> 
-      print_string "("; 
-      box_display c; 
+      print_cut(); box_display c;
+  | App (c,l) ->
+      print_string "(";
+      box_display c;
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string ")"
   | Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{";
@@ -258,25 +258,25 @@ let print_pure_constr csr =
       open_vbox 0;
       Array.iter (fun x ->  print_cut();  box_display x) bl;
       close_box();
-      print_cut(); 
-      print_string "end"; 
+      print_cut();
+      print_string "end";
       close_box()
   | Fix ((t,i),(lna,tl,bl)) ->
-      print_string "Fix("; print_int i; print_string ")"; 
+      print_string "Fix("; print_int i; print_string ")";
       print_cut();
       open_vbox 0;
       let rec print_fix () =
         for k = 0 to (Array.length tl) - 1 do
 	  open_vbox 0;
-	  name_display lna.(k); print_string "/"; 
+	  name_display lna.(k); print_string "/";
 	  print_int t.(k); print_cut(); print_string ":";
 	  box_display tl.(k) ; print_cut(); print_string ":=";
 	  box_display bl.(k); close_box ();
 	  print_cut()
         done
-      in print_string"{"; print_fix(); print_string"}" 
+      in print_string"{"; print_fix(); print_string"}"
   | CoFix(i,(lna,tl,bl)) ->
-      print_string "CoFix("; print_int i; print_string ")"; 
+      print_string "CoFix("; print_int i; print_string ")";
       print_cut();
       open_vbox 0;
       let rec print_fix () =
@@ -301,27 +301,27 @@ let print_pure_constr csr =
     | Name id -> print_string (string_of_id id)
     | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)
-  and sp_display sp = 
+  and sp_display sp =
 (*    let dir,l = decode_kn sp in
-    let ls = 
-      match List.rev (List.map string_of_id (repr_dirpath dir)) with 
+    let ls =
+      match List.rev (List.map string_of_id (repr_dirpath dir)) with
           ("Top"::l)-> l
-	| ("Coq"::_::l) -> l 
+	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
       print_string (string_of_kn sp)
-  and sp_con_display sp = 
+  and sp_con_display sp =
 (*    let dir,l = decode_kn sp in
-    let ls = 
-      match List.rev (List.map string_of_id (repr_dirpath dir)) with 
+    let ls =
+      match List.rev (List.map string_of_id (repr_dirpath dir)) with
           ("Top"::l)-> l
-	| ("Coq"::_::l) -> l 
+	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
       print_string (string_of_con sp)
 
   in
-    try 
+    try
      box_display csr; print_flush()
     with e ->
 	print_string (Printexc.to_string e);print_flush ();
@@ -370,7 +370,7 @@ let pp_generic_argument arg =
 (* Vernac-level debugging commands                                    *)
 
 let in_current_context f c =
-  let (evmap,sign) = 
+  let (evmap,sign) =
     try Pfedit.get_current_goal_context ()
     with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in
   f (Constrintern.interp_constr evmap sign c)
@@ -431,26 +431,26 @@ open Libnames
 let encode_path loc prefix mpdir suffix id =
   let dir = match mpdir with
     | None -> []
-    | Some (mp,dir) -> 
+    | Some (mp,dir) ->
 	(repr_dirpath (dirpath_of_string (string_of_mp mp))@
 	repr_dirpath dir) in
-  Qualid (loc, make_qualid 
+  Qualid (loc, make_qualid
     (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
 
 let raw_string_of_ref loc = function
-  | ConstRef cst -> 
+  | ConstRef cst ->
       let (mp,dir,id) = repr_con cst in
       encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)
   | IndRef (kn,i) ->
       let (mp,dir,id) = repr_kn kn in
-      encode_path loc "IND" (Some (mp,dir)) [id_of_label id] 
+      encode_path loc "IND" (Some (mp,dir)) [id_of_label id]
 	(id_of_string ("_"^string_of_int i))
-  | ConstructRef ((kn,i),j) -> 
+  | ConstructRef ((kn,i),j) ->
       let (mp,dir,id) = repr_kn kn in
       encode_path loc "CSTR" (Some (mp,dir))
-	[id_of_label id;id_of_string ("_"^string_of_int i)] 
+	[id_of_label id;id_of_string ("_"^string_of_int i)]
 	(id_of_string ("_"^string_of_int j))
-  | VarRef id -> 
+  | VarRef id ->
       encode_path loc "SECVAR" None [] id
 
 let short_string_of_ref loc = function
@@ -460,8 +460,8 @@ let short_string_of_ref loc = function
   | IndRef (kn,i) ->
       encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))]
         (id_of_string ("_"^string_of_int i))
-  | ConstructRef ((kn,i),j) -> 
-      encode_path loc "CSTR" None 
+  | ConstructRef ((kn,i),j) ->
+      encode_path loc "CSTR" None
         [id_of_label (pi3 (repr_kn kn));id_of_string ("_"^string_of_int i)]
         (id_of_string ("_"^string_of_int j))
 
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 1e1144895f..266bd1043c 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -7,9 +7,9 @@ open Vm
 
 let ppripos (ri,pos) =
   (match ri with
-  | Reloc_annot a -> 
+  | Reloc_annot a ->
       let sp,i = a.ci.ci_ind in
-      print_string 
+      print_string
 	("annot : MutInd("^(string_of_kn sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
@@ -29,8 +29,8 @@ let ppsort = function
 
 
 let print_idkey idk =
-  match idk with 
-  | ConstKey sp -> 
+  match idk with
+  | ConstKey sp ->
       print_string "Cons(";
       print_string (string_of_con sp);
       print_string ")"
@@ -38,8 +38,8 @@ let print_idkey idk =
   | RelKey i -> print_string "~";print_int i
 
 let rec ppzipper z =
-  match z with 
-  | Zapp args -> 
+  match z with
+  | Zapp args ->
       let n = nargs args in
       open_hbox ();
       for i = 0 to n-2 do
@@ -50,7 +50,7 @@ let rec ppzipper z =
   | Zfix _ -> print_string "Zfix"
   | Zswitch _ -> print_string "Zswitch"
 
-and ppstack s = 
+and ppstack s =
   open_hovbox 0;
   print_string "[";
   List.iter (fun z -> ppzipper z;print_string " | ") s;
@@ -67,14 +67,14 @@ and ppatom a =
       print_string ")"
 
 and ppwhd whd =
-  match whd with 
+  match whd with
   | Vsort s -> ppsort s
   | Vprod _ -> print_string "product"
   | Vfun _ -> print_string "function"
   | Vfix _ -> print_vfix()
   | Vcofix _ -> print_string "cofix"
   | Vconstr_const i -> print_string "C(";print_int i;print_string")"
-  | Vconstr_block b -> ppvblock b      
+  | Vconstr_block b -> ppvblock b
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s