Removal of trailing spaces.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 40 insertions, 40 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index d75a996ef..eb410b1e3 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -423,7 +423,7 @@ let record_interp cmd_stk start_of_sentence end_of_sentence (sn,pp,psd) =
   } cmd_stk
 
 let backtrack cmd_stack stop_cond =
-  if Stack.is_empty cmd_stack then 
+  if Stack.is_empty cmd_stack then
     reset_initial () (* reset coq *)
   else try
     let current = Stack.top cmd_stack in
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 576c20997..59681e8f1 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Names
 open Term
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 928aa3e09..3b27b0171 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -160,7 +160,7 @@ let mkTacCase with_evar = function
   | [([ElimOnIdent id],None,(None,None))],None ->
       TacCase (with_evar,(CRef (Ident id),NoBindings))
   | ic ->
-      if List.exists (fun (cl,a,b) -> 
+      if List.exists (fun (cl,a,b) ->
            List.exists (function ElimOnAnonHyp _ -> true | _ -> false) cl)
            (fst ic)
       then
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 0e960146c..cc667aa05 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -690,8 +690,8 @@ let parse_q term =
 		  begin
 		    try
 		      let (expr,env) = parse_expr env args.(0) in
-		      let power = (parse_exp expr args.(1)) in 
-			(power  , env) 
+		      let power = (parse_exp expr args.(1)) in
+			(power  , env)
 		    with _ ->   (* if the exponent is a variable *)
 		      let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
 		  end
@@ -753,21 +753,21 @@ let rconstant term =
   |  _ -> raise ParseError
 
 
-let parse_zexpr =  parse_expr 
-   zconstant 
-   (fun expr x -> 
+let parse_zexpr =  parse_expr
+   zconstant
+   (fun expr x ->
      let exp = (parse_z x) in
        match exp with
 	 | Mc.Zneg _ -> Mc.PEc Mc.Z0
 	 |   _     ->  Mc.PEpow(expr, Mc.n_of_Z exp))
-   zop_spec 
+   zop_spec
 
-let parse_qexpr  =  parse_expr 
-  qconstant 
-   (fun expr x -> 
+let parse_qexpr  =  parse_expr
+  qconstant
+   (fun expr x ->
      let exp = parse_z x in
        match exp with
-	 | Mc.Zneg _ -> 
+	 | Mc.Zneg _ ->
 	     begin
 	       match expr with
 	       | Mc.PEc q -> Mc.PEc (Mc.qpower q exp)
@@ -775,18 +775,18 @@ let parse_qexpr  =  parse_expr
 	     end
 	 | _     ->  let exp = Mc.n_of_Z  exp in
 		       Mc.PEpow(expr,exp))
-  qop_spec 
+  qop_spec
 
-let parse_rexpr =  parse_expr 
-  rconstant  
-  (fun expr x -> 
+let parse_rexpr =  parse_expr
+  rconstant
+  (fun expr x ->
      let exp = Mc.n_of_nat (parse_nat x) in
-       Mc.PEpow(expr,exp))  
+       Mc.PEpow(expr,exp))
   rop_spec
 
 
- let  parse_arith parse_op parse_expr env cstr = 
-  if debug 
+ let  parse_arith parse_op parse_expr env cstr =
+  if debug
   then (Pp.pp_flush ();
 	Pp.pp (Pp.str "parse_arith: ");
 	Pp.pp (Printer.prterm  cstr);
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6ecbb09c4..9cdbc6627 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -655,7 +655,7 @@ let print_applicable_hint () =
 let print_hint_db db =
   let (ids, csts) = Hint_db.transparent_state db in
   msg (hov 0
-	  ((if Hint_db.use_dn db then str"Discriminated database" 
+	  ((if Hint_db.use_dn db then str"Discriminated database"
 	    else str"Non-discriminated database") ++ fnl ()));
   msg (hov 0
 	  (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6d1c91634..a5adb9169 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -82,7 +82,7 @@ let evars_to_goals p evm =
     else
       let goals = List.rev goals in
 	Some (goals, evm')
-	  
+
 (** Typeclasses instance search tactic / eauto *)
 
 let intersects s t =
@@ -281,7 +281,7 @@ let hints_tac hints =
       in
 	if l = [] && !typeclasses_debug then
 	  msgnl (pr_depth info.auto_depth ++ str": no match for " ++
-		    Printer.pr_constr_env (Evd.evar_env gl) concl ++ 
+		    Printer.pr_constr_env (Evd.evar_env gl) concl ++
 		    spc () ++ int (List.length poss) ++ str" possibilities");
 	List.map possible_resolve l
     in
@@ -387,10 +387,10 @@ let run_on_evars ?(st=full_transparent_state) p evm tac =
 	    Some (Evd.evars_reset_evd evm' evm)
 
 
-let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints)) 
+let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints))
 
 let () = run_on_evars_forward := (fun hints st p evd -> run_on_evars ~st p evd (eauto_tac hints))
-  
+
 let eauto hints g =
   let gl = { it = make_autogoal ~st:(Hint_db.transparent_state (List.hd hints)) g; sigma = project g } in
     match run_tac (eauto_tac hints) gl with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 302c84a5e..2a4fc6a0f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2481,7 +2481,7 @@ let compute_elim_sig ?elimc elimt =
 	  try {!res with indref = Some (global_of_constr indhd) }
 	  with _ -> error "Cannot find the inductive type of the inductive scheme.";;
 
-let compute_scheme_signature scheme names_info ind_type_guess = 
+let compute_scheme_signature scheme names_info ind_type_guess =
   let f,l = decompose_app scheme.concl in
   (* Vérifier que les arguments de Qi sont bien les xi. *)
   match scheme.indarg with
@@ -2582,7 +2582,7 @@ let guess_elim isrec hyp0 gl =
     else
       let case =
 	if !dependent_propositions_elimination &&
-	   dependent_no_evar (mkVar hyp0) (pf_concl gl) 
+	   dependent_no_evar (mkVar hyp0) (pf_concl gl)
 	then make_case_dep
 	else make_case_gen in
       pf_apply case gl mind s in
@@ -2607,7 +2607,7 @@ type eliminator =
   | ElimOver of bool * identifier
 
 let find_induction_type isrec elim hyp0 gl =
-  let scheme,elim = 
+  let scheme,elim =
     match elim with
     | None ->
 	let (elimc,elimt),_ = guess_elim isrec hyp0 gl in
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 21806269a..5084635e8 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -21,9 +21,9 @@ open Nametab
    See the module dn.ml for further explanations.
    Eduardo (5/8/97) *)
 
-type term_label = 
+type term_label =
   | GRLabel of global_reference
-  | ProdLabel 
+  | ProdLabel
   | LambdaLabel
   | SortLabel of sorts option
 
@@ -68,7 +68,7 @@ let constr_pat_discr_st (idpred,cpred) t =
       Some (GRLabel ref, args)
   | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
   | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l)
-  | PSort s, [] -> 
+  | PSort s, [] ->
       let s' = match s with
 	| RProp c -> Some (Prop c)
 	| RType (Some c) -> Some (Type c)
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index f3743b128..e60aea6b4 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -48,9 +48,9 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 (*i*)
 (* These are for Nbtermdn *)
 
-type term_label = 
+type term_label =
   | GRLabel of global_reference
-  | ProdLabel 
+  | ProdLabel
   | LambdaLabel
   | SortLabel of sorts option
 
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index e8a68c11d..5091b44c1 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -115,7 +115,7 @@ inversion H.
 
 Fixpoint prodn (n : nat) :=
   match n with
-  | O => unit 
+  | O => unit
   | (S m) => prod (prodn m) nat
   end.
 
diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v
index 71054e141..0a0812711 100644
--- a/test-suite/success/autointros.v
+++ b/test-suite/success/autointros.v
@@ -9,7 +9,7 @@ with odd : nat -> Prop :=
 
 Lemma foo {n : nat} (E : even n) : even (S (S n))
 with bar {n : nat} (O : odd n) : odd (S (S n)).
-Proof. destruct E. constructor. constructor. apply even_odd. apply (bar _ H). 
-  destruct O. repeat constructor. apply odd_even. apply (foo _ H). 
+Proof. destruct E. constructor. constructor. apply even_odd. apply (bar _ H).
+  destruct O. repeat constructor. apply odd_even. apply (foo _ H).
 Defined.
 
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 7adcc8de3..8013e1d38 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -67,7 +67,7 @@ Abort.
 Variable A0:Type.
 Variable P:A0->Type.
 Require Import JMeq.
-Goal forall a b (p:P a) (q:P b), 
+Goal forall a b (p:P a) (q:P b),
   forall H:a = b, eq_rect a P p b H = q -> JMeq (existT _ a p) (existT _ b q).
 intros.
 destruct H.
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
index 357e5e212..c9fb56292 100644
--- a/theories/Reals/Rpow_def.v
+++ b/theories/Reals/Rpow_def.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 Require Import Rdefinitions.
 
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 08c0bac1c..0186c6982 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -50,7 +50,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
   | Anomaly (s,pps) ->
       hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
   | AnomalyOnError (s,exc) ->
-      hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++ 
+      hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++
 	fnl() ++ explain_exn_default_aux anomaly_string report_fn exc)
   | Match_failure(filename,pos1,pos2) ->
       hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1086e8419..b50bcca77 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1235,7 +1235,7 @@ let start_proof_com kind thms hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  hook strength ref) thms_data in
-      let init_tac = 
+      let init_tac =
 	let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
 	  if Flags.is_auto_intros () then
 	    match rec_tac with