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

diff --git a/ide/coq.ml b/ide/coq.ml
index 4fd48a3064..a567fb4f54 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -30,16 +30,16 @@ let prerr_endline s = if !debug then prerr_endline s else ()
 
 let output = ref (Format.formatter_of_out_channel stdout)
 
-let msg m = 
+let msg m =
   let b =  Buffer.create 103 in
   Pp.msg_with (Format.formatter_of_buffer b) m;
   Buffer.contents b
 
-let msgnl m = 
+let msgnl m =
   (msg m)^"\n"
 
-let init () = 
-  (* To hide goal in lower window. 
+let init () =
+  (* To hide goal in lower window.
      Problem: should not hide "xx is assumed"
      messages *)
 (**)
@@ -70,7 +70,7 @@ let short_version () =
 
 let version () =
   let (ver,date) = get_version_date () in
-    Printf.sprintf 
+    Printf.sprintf
       "The Coq Proof Assistant, version %s (%s)\
        \nArchitecture %s running %s operating system\
        \nGtk version is %s\
@@ -79,14 +79,14 @@ let version () =
       ver date
       Coq_config.arch Sys.os_type
       (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
-    (if Mltop.is_native then "native" else "bytecode") 
-    (if Coq_config.best="opt" then "native" else "bytecode") 
+    (if Mltop.is_native then "native" else "bytecode")
+    (if Coq_config.best="opt" then "native" else "bytecode")
 
-let is_in_coq_lib dir = 
+let is_in_coq_lib dir =
   prerr_endline ("Is it a coq theory ? : "^dir);
   let is_same_file = same_file dir in
-  List.exists 
-    (fun s -> 
+  List.exists
+    (fun s ->
       let fdir =
         Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in
       prerr_endline (" Comparing to: "^fdir);
@@ -97,19 +97,19 @@ let is_in_coq_lib dir =
 let is_in_loadpath dir =
   Library.is_in_load_paths (System.physical_path_of_string dir)
 
-let is_in_coq_path f = 
-  try 
+let is_in_coq_path f =
+  try
   let base = Filename.chop_extension (Filename.basename f) in
   let _ = Library.locate_qualified_library false
-	    (Libnames.make_qualid Names.empty_dirpath 
+	    (Libnames.make_qualid Names.empty_dirpath
 	       (Names.id_of_string base)) in
   prerr_endline (f ^ " is in coq path");
   true
-  with _ ->  
+  with _ ->
     prerr_endline (f ^ " is NOT in coq path");
-    false  
+    false
 
-let is_in_proof_mode () = 
+let is_in_proof_mode () =
   match Decl_mode.get_current_mode () with
       Decl_mode.Mode_none -> false
     | _ -> true
@@ -347,13 +347,13 @@ type reset_info = reset_mark * undo_info * bool ref
 
 let compute_reset_info () =
   (match Lib.has_top_frozen_state () with
-    | Some st -> 
+    | Some st ->
 	prerr_endline ("On top of state "^Libnames.string_of_path (fst st));
 	st
-    | None -> 
+    | None ->
 	failwith "FATAL ERROR: NO RESET"), undo_info(), ref true
 
-let reset_initial () = 
+let reset_initial () =
   prerr_endline "Reset initial called"; flush stderr;
   Vernacentries.abort_refine Lib.reset_initial ()
 
@@ -361,14 +361,14 @@ let reset_to st =
   prerr_endline ("Reset called with state "^(Libnames.string_of_path (fst st)));
   Lib.reset_to_state st
 
-let reset_to_mod id = 
-  prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); 
+let reset_to_mod id =
+  prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id));
   Lib.reset_mod (Util.dummy_loc,id)
 
 let raw_interp s =
   Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s))
 
-let interp_with_options verbosely options s = 
+let interp_with_options verbosely options s =
   prerr_endline "Starting interp...";
   prerr_endline s;
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
@@ -376,7 +376,7 @@ let interp_with_options verbosely options s =
   (* Temporary hack to make coqide.byte work (WTF???) - now with less screen
   * pollution *)
   Pervasives.prerr_string " \r"; Pervasives.flush stderr;
-  match pe with 
+  match pe with
     | None -> assert false
     | Some((loc,vernac) as last) ->
 	if is_vernac_debug_command vernac then
@@ -385,7 +385,7 @@ let interp_with_options verbosely options s =
 	  user_error_loc loc (str "Use CoqIDE navigation instead");
 	if is_vernac_known_option_command vernac then
 	  user_error_loc loc (str "Use CoqIDE display menu instead");
-	if is_vernac_query_command vernac then 
+	if is_vernac_query_command vernac then
 	  flash_info
 	    "Warning: query commands should not be inserted in scripts";
 	if not (is_vernac_goal_printing_command vernac) then
@@ -402,12 +402,12 @@ let interp_with_options verbosely options s =
 let interp verbosely phrase =
   interp_with_options verbosely (make_option_commands ()) phrase
 
-let interp_and_replace s = 
+let interp_and_replace s =
   let result = interp false s in
   let msg = read_stdout () in
   result,msg
 
-type tried_tactic = 
+type tried_tactic =
   | Interrupted
   | Success of int (* nb of goals after *)
   | Failed
@@ -424,7 +424,7 @@ let print_toplevel_error exc =
     match exc with
       | DuringCommandInterp (loc,ie) ->
           if loc = dummy_loc then (None,ie) else (Some loc, ie)
-      | _ -> (None, exc) 
+      | _ -> (None, exc)
   in
   let (loc,exc) =
     match exc with
@@ -434,19 +434,19 @@ let print_toplevel_error exc =
   in
   match exc with
     | End_of_input  -> 	str "Please report: End of input",None
-    | Vernacexpr.ProtectedLoop -> 
+    | Vernacexpr.ProtectedLoop ->
 	str "ProtectedLoop  not allowed by coqide!",None
     | Vernacexpr.Drop ->  str "Drop is not allowed by coqide!",None
     | Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None
-    | _ -> 
-	(try Cerrors.explain_exn exc with e -> 
+    | _ ->
+	(try Cerrors.explain_exn exc with e ->
 	   str "Failed to explain error. This is an internal Coq error. Please report.\n"
 	   ++ str (Printexc.to_string  e)),
 	(if is_pervasive_exn exc then None else loc)
 
 let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
 
-let interp_last last = 
+let interp_last last =
   prerr_string "*";
   try
     vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
@@ -457,7 +457,7 @@ let interp_last last =
 
 
 type hyp = env * evar_map *
-           ((identifier * string) * constr option * constr) * 
+           ((identifier * string) * constr option * constr) *
            (string * string)
 type concl = env * evar_map * constr * string
 type meta = env * evar_map * string
@@ -465,7 +465,7 @@ type goal = hyp list * concl
 
 let prepare_hyp sigma env ((i,c,d) as a) =
   env, sigma,
-  ((i,string_of_id i),c,d), 
+  ((i,string_of_id i),c,d),
   (msg (pr_var_decl env a), msg (pr_ltype_env env d))
 
 let prepare_hyps sigma env =
@@ -473,7 +473,7 @@ let prepare_hyps sigma env =
   let hyps =
     fold_named_context
       (fun env d acc -> let hyp = prepare_hyp sigma env d in hyp :: acc)
-      env ~init:[] 
+      env ~init:[]
   in
   List.rev hyps
 
@@ -496,9 +496,9 @@ let get_current_pm_goal () =
   let gl = sig_it gls in
     prepare_goal sigma gl
 
-let get_current_goals () = 
+let get_current_goals () =
     let pfts = get_pftreestate () in
-    let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
+    let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
     let sigma = Tacmach.evc_of_pftreestate pfts in
     List.map (prepare_goal sigma) gls
 
@@ -508,16 +508,16 @@ let print_no_goal () =
 
 let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
   [("clear "^ident),("clear "^ident^".");
-   
+
    ("apply "^ident),
    ("apply "^ident^".");
-   
+
    ("exact "^ident),
    ("exact "^ident^".");
 
    ("generalize "^ident),
    ("generalize "^ident^".");
-   
+
    ("absurd <"^ident^">"),
    ("absurd "^
     pr_ast
@@ -528,34 +528,34 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
 	"injection "^ident, "injection "^ident^"." ]
     else
       []) @
-   
+
    (let _,t = splay_prod env sigma ast in
-    if is_equality_type t then 
+    if is_equality_type t then
       [ "rewrite "^ident, "rewrite "^ident^".";
 	"rewrite <- "^ident, "rewrite <- "^ident^"." ]
     else
       []) @
-   
+
   [("elim "^ident),
    ("elim "^ident^".");
-   
+
    ("inversion "^ident),
    ("inversion "^ident^".");
-   
+
    ("inversion clear "^ident),
-   ("inversion_clear "^ident^".")] 
+   ("inversion_clear "^ident^".")]
 
-let concl_menu (_,_,concl,_) = 
+let concl_menu (_,_,concl,_) =
   let is_eq = is_equality_type concl in
   ["intro", "intro.";
    "intros", "intros.";
    "intuition","intuition." ] @
-   
-   (if is_eq then 
+
+   (if is_eq then
       ["reflexivity", "reflexivity.";
        "discriminate", "discriminate.";
        "symmetry", "symmetry." ]
-    else 
+    else
       []) @
 
   ["assumption" ,"assumption.";
@@ -577,41 +577,41 @@ let concl_menu (_,_,concl,_) =
   ]
 
 
-let id_of_name = function 
-  | Names.Anonymous -> id_of_string "x" 
+let id_of_name = function
+  | Names.Anonymous -> id_of_string "x"
   | Names.Name x -> x
 
-let make_cases s = 
+let make_cases s =
   let qualified_name = Libnames.qualid_of_string s in
   let glob_ref = Nametab.locate qualified_name in
   match glob_ref with
-    | Libnames.IndRef i -> 
+    | Libnames.IndRef i ->
 	let {Declarations.mind_nparams = np},
 	{Declarations.mind_consnames = carr ;
-	 Declarations.mind_nf_lc = tarr } 
-	= Global.lookup_inductive i 
+	 Declarations.mind_nf_lc = tarr }
+	= Global.lookup_inductive i
 	in
-	Util.array_fold_right2 
-	  (fun n t l ->  
+	Util.array_fold_right2
+	  (fun n t l ->
 	     let (al,_) = Term.decompose_prod t in
 	     let al,_ = Util.list_chop (List.length al - np) al in
-	     let rec rename avoid = function 
+	     let rec rename avoid = function
 	       | [] -> []
-	       | (n,_)::l -> 
+	       | (n,_)::l ->
 		   let n' = next_global_ident_away true
-			      (id_of_name n) 
+			      (id_of_name n)
 			      avoid
 		   in (string_of_id n')::(rename (n'::avoid) l)
 	     in
 	     let al' = rename [] (List.rev al) in
 	     (string_of_id n :: al') :: l
 	  )
-	  carr 
+	  carr
 	  tarr
 	  []
     | _ -> raise Not_found
 
-let current_status () = 
+let current_status () =
   let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
   let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
   try