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

diff --git a/parsing/printer.ml b/parsing/printer.ml
index b23f94a70f..eacad74c4c 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -29,11 +29,11 @@ open Ppconstr
 open Constrextern
 open Tacexpr
 
-let emacs_str s alts = 
+let emacs_str s alts =
   match !Flags.print_emacs, !Flags.print_emacs_safechar with
     | true, true -> alts
     | true , false -> s
-    | false,_ -> "" 
+    | false,_ -> ""
 
 (**********************************************************************)
 (** Terms                                                             *)
@@ -77,7 +77,7 @@ let pr_ljudge j = pr_ljudge_env (Global.env()) j
 
 let pr_lrawconstr_env env c =
   pr_lconstr_expr (extern_rawconstr (vars_of_env env) c)
-let pr_rawconstr_env env c = 
+let pr_rawconstr_env env c =
   pr_constr_expr (extern_rawconstr (vars_of_env env) c)
 
 let pr_lrawconstr c =
@@ -130,7 +130,7 @@ let pr_var_decl env (id,c,typ) =
   let pbody = match c with
     | None ->  (mt ())
     | Some c ->
-	(* Force evaluation *) 
+	(* Force evaluation *)
 	let pb = pr_lconstr_env env c in
 	let pb = if isCast c then surround pb else pb in
 	(str" := " ++ pb ++ cut () ) in
@@ -142,7 +142,7 @@ let pr_rel_decl env (na,c,typ) =
   let pbody = match c with
     | None -> mt ()
     | Some c ->
-	(* Force evaluation *) 
+	(* Force evaluation *)
 	let pb = pr_lconstr_env env c in
 	let pb = if isCast c then surround pb else pb in
 	(str":=" ++ spc () ++ pb ++ spc ()) in
@@ -162,7 +162,7 @@ let pr_named_context_of env =
   let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
   hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
-let pr_named_context env ne_context = 
+let pr_named_context env ne_context =
   hv 0 (Sign.fold_named_context
 	  (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d)
           ne_context ~init:(mt ()))
@@ -179,14 +179,14 @@ let pr_context_unlimited env =
     fold_named_context
       (fun env d pps ->
          let pidt =  pr_var_decl env d in (pps ++ fnl () ++ pidt))
-      env ~init:(mt ()) 
+      env ~init:(mt ())
   in
   let db_env =
     fold_rel_context
       (fun env d pps ->
          let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
       env ~init:(mt ())
-  in 
+  in
   (sign_env ++ db_env)
 
 let pr_ne_context_of header env =
@@ -197,21 +197,21 @@ let pr_ne_context_of header env =
 let pr_context_limit n env =
   let named_context = Environ.named_context env in
   let lgsign = List.length named_context in
-  if n >= lgsign then 
+  if n >= lgsign then
     pr_context_unlimited env
   else
     let k = lgsign-n in
     let _,sign_env =
       fold_named_context
         (fun env d (i,pps) ->
-           if i < k then 
+           if i < k then
 	     (i+1, (pps ++str "."))
 	   else
              let pidt = pr_var_decl env d in
 	     (i+1, (pps ++ fnl () ++
 		      str (emacs_str (String.make 1 (Char.chr 253)) "") ++
 		      pidt)))
-        env ~init:(0,(mt ())) 
+        env ~init:(0,(mt ()))
     in
     let db_env =
       fold_rel_context
@@ -221,10 +221,10 @@ let pr_context_limit n env =
 	      str (emacs_str (String.make 1 (Char.chr 253)) "") ++
 	      pnat))
         env ~init:(mt ())
-    in 
+    in
     (sign_env ++ db_env)
 
-let pr_context_of env = match Flags.print_hyps_limit () with 
+let pr_context_of env = match Flags.print_hyps_limit () with
   | None -> hv 0 (pr_context_unlimited env)
   | Some n -> hv 0 (pr_context_limit n env)
 
@@ -234,33 +234,33 @@ let pr_restricted_named_context among env =
   hv 0 (fold_named_context
 	  (fun env ((id,_,_) as d) pps ->
 	     if true || Idset.mem id among then
-	       pps ++ 
+	       pps ++
 		 fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++
 		 pr_var_decl env d
-	     else 
+	     else
 	       pps)
           env ~init:(mt ()))
 
 
-let pr_predicate pr_elt (b, elts) = 
+let pr_predicate pr_elt (b, elts) =
   let pr_elts = prlist_with_sep spc pr_elt elts in
     if b then
-      str"all" ++ 
+      str"all" ++
 	(if elts = [] then mt () else str" except: " ++ pr_elts)
     else
       if elts = [] then str"none" else pr_elts
-      
+
 let pr_cpred p = pr_predicate pr_con (Cpred.elements p)
 let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p)
 
-let pr_transparent_state (ids, csts) = 
+let pr_transparent_state (ids, csts) =
   hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
 	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
 
 let pr_subgoal_metas metas env=
-  let pr_one (meta,typ) = 
-    str "?" ++ int meta ++ str " : " ++ 
-      hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ 
+  let pr_one (meta,typ) =
+    str "?" ++ int meta ++ str " : " ++
+      hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++
       str (emacs_str (String.make 1 (Char.chr 253)) "") in
     hv 0 (prlist_with_sep mt pr_one metas)
 
@@ -272,7 +272,7 @@ let default_pr_goal g =
           mt (), mt (),
 	  pr_context_of env,
 	  pr_ltype_env_at_top env g.evar_concl
-    else 
+    else
       (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
       (str "thesis := "  ++ fnl ()),
        pr_context_of env,
@@ -283,7 +283,7 @@ let default_pr_goal g =
 		       str (emacs_str (String.make 1 (Char.chr 253)) "")  ++
 		       str "============================" ++ fnl ()  ++
 		       thesis ++ str " " ++  pc) ++ fnl ()
-     
+
 (* display the conclusion of a goal *)
 let pr_concl n g =
   let env = evar_env g in
@@ -292,7 +292,7 @@ let pr_concl n g =
       str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
 
 (* display evar type: a context and a type *)
-let pr_evgl_sign gl = 
+let pr_evgl_sign gl =
   let ps = pr_named_context_of (evar_unfiltered_env gl) in
   let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
   let ids = List.rev (List.map pi1 l) in
@@ -307,10 +307,10 @@ let pr_evgl_sign gl =
 let rec pr_evars_int i = function
   | [] -> (mt ())
   | (ev,evd)::rest ->
-      let pegl = pr_evgl_sign evd in 
+      let pegl = pr_evgl_sign evd in
       let pei = pr_evars_int (i+1) rest in
       (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
-              str (string_of_existential ev)  ++ str " : " ++ pegl)) ++ 
+              str (string_of_existential ev)  ++ str " : " ++ pegl)) ++
       fnl () ++ pei
 
 let default_pr_subgoal n =
@@ -320,22 +320,22 @@ let default_pr_subgoal n =
        	if p = 1 then
           let pg = default_pr_goal g in
           v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
-       	else 
+       	else
 	  prrec (p-1) rest
-  in 
+  in
   prrec n
 
 (* Print open subgoals. Checks for uninstantiated existential variables *)
-let default_pr_subgoals close_cmd sigma = function 
-  | [] -> 
+let default_pr_subgoals close_cmd sigma = function
+  | [] ->
       begin
 	match close_cmd with
 	  Some cmd ->
-	    (str "Subproof completed, now type " ++ str cmd ++ 
+	    (str "Subproof completed, now type " ++ str cmd ++
 	       str "." ++ fnl ())
 	| None ->
-	    let exl = Evarutil.non_instantiated sigma in 
-	      if exl = [] then 
+	    let exl = Evarutil.non_instantiated sigma in
+	      if exl = [] then
 		(str"Proof completed." ++ fnl ())
 	      else
 		let pei = pr_evars_int 1 exl in
@@ -351,11 +351,11 @@ let default_pr_subgoals close_cmd sigma = function
         | g::rest ->
             let pc = pr_concl n g in
             let prest = pr_rec (n+1) rest in
-            (cut () ++ pc ++ prest) 
+            (cut () ++ pc ++ prest)
       in
       let pg1 = default_pr_goal g1 in
       let prest = pr_rec 2 rest in
-      v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
+      v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
 	   ++ pg1 ++ prest ++ fnl ())
 
 
@@ -388,17 +388,17 @@ let pr_goal     x = !printer_pr.pr_goal     x
 
 let pr_open_subgoals () =
   let pfts = get_pftreestate () in
-  let gls = fst (frontier (proof_of_pftreestate pfts)) in 
+  let gls = fst (frontier (proof_of_pftreestate pfts)) in
   match focus() with
-    | 0 -> 
+    | 0 ->
         let sigma = (top_goal_of_pftreestate pfts).sigma in
         let close_cmd = Decl_mode.get_end_command pfts in
         pr_subgoals close_cmd sigma gls
-    | n -> 
+    | n ->
 	assert (n > List.length gls);
-	if List.length gls < 2 then 
+	if List.length gls < 2 then
 	  pr_subgoal n gls
-	else 
+	else
 	  (* LEM TODO: this way of saying how many subgoals has to be abstracted out*)
 	  v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
 	  pr_subgoal n gls)
@@ -410,25 +410,25 @@ let pr_nth_open_subgoal n =
 (* Elementary tactics *)
 
 let pr_prim_rule = function
-  | Intro id -> 
+  | Intro id ->
       str"intro " ++ pr_id id
-	
+
   | Cut (b,replace,id,t) ->
      if b then
        (* TODO: express "replace" *)
        (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")")
      else
        let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in
-       (str"cut " ++ pr_constr t ++ 
+       (str"cut " ++ pr_constr t ++
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
-	
+
   | FixRule (f,n,[],_) ->
       (str"fix " ++ pr_id f ++ str"/" ++ int n)
-      
-  | FixRule (f,n,others,j) -> 
+
+  | FixRule (f,n,others,j) ->
       if j<>0 then warning "Unsupported printing of \"fix\"";
       let rec print_mut = function
-	| (f,n,ar)::oth -> 
+	| (f,n,ar)::oth ->
            pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
         | [] -> mt () in
       (str"fix " ++ pr_id f ++ str"/" ++ int n ++
@@ -444,26 +444,26 @@ let pr_prim_rule = function
 	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
         | [] -> mt () in
       (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
-  | Refine c -> 
+  | Refine c ->
       str(if occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
-      
+
   | Convert_concl (c,_) ->
       (str"change "  ++ pr_constr c)
-      
+
   | Convert_hyp (id,None,t) ->
       (str"change "  ++ pr_constr t  ++ spc ()  ++ str"in "  ++ pr_id id)
 
   | Convert_hyp (id,Some c,t) ->
       (str"change "  ++ pr_constr c  ++ spc ()  ++ str"in "
        ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
-      
+
   | Thin ids ->
       (str"clear "  ++ prlist_with_sep pr_spc pr_id ids)
-      
+
   | ThinBody ids ->
       (str"clearbody "  ++ prlist_with_sep pr_spc pr_id ids)
-      
+
   | Move (withdep,id1,id2) ->
       (str (if withdep then "dependent " else "") ++
 	 str"move "  ++ pr_id id1 ++ pr_move_location pr_id id2)
@@ -488,7 +488,7 @@ let prterm = pr_lconstr
 
 (* spiwack: printer function for sets of Environ.assumption.
             It is used primarily by the Print Assumption command. *)
-let pr_assumptionset env s = 
+let pr_assumptionset env s =
   if (Environ.ContextObjectMap.is_empty s) then
     str "Closed under the global context"
   else
@@ -497,7 +497,7 @@ let pr_assumptionset env s =
 	let (v,a,o) = r in
 	match t with
 	| Variable id -> (  Some (
-	                      Option.default (fnl ()) v 
+	                      Option.default (fnl ()) v
 			   ++ str (string_of_id id)
 			   ++ str " : "
 	                   ++ pr_ltype typ
@@ -527,7 +527,7 @@ let pr_assumptionset env s =
       )
 	s (None,None,None)
     in
-    let (vars,axioms,opaque) = 
+    let (vars,axioms,opaque) =
       ( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
 	Option.map (fun p -> str "Axioms:" ++ p) axioms ,
 	Option.map (fun p -> str "Opaque constants:" ++ p) opaque
@@ -540,9 +540,9 @@ let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
 
 open Typeclasses
 
-let pr_instance i = 
+let pr_instance i =
   pr_global (ConstRef (instance_impl i))
-    
+
 let pr_instance_gmap insts =
   prlist_with_sep fnl (fun (gr, insts) ->
     prlist_with_sep fnl pr_instance (cmap_to_list insts))