Removal of trailing spaces.

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

5 files changed, 13 insertions, 13 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6ecbb09c41..9cdbc66278 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 6d1c916348..a5adb9169b 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 302c84a5ea..2a4fc6a0f5 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 21806269af..5084635e80 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 f3743b1280..e60aea6b43 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