Strip some trailing spaces

4 files changed, 28 insertions, 28 deletions

diff --git a/Makefile.build b/Makefile.build
index fc92507e6..44eb42f9a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -78,8 +78,8 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 
-# The SHOW and HIDE variables control whether make will echo complete commands 
-# or only abbreviated versions. 
+# The SHOW and HIDE variables control whether make will echo complete commands
+# or only abbreviated versions.
 # Quiet mode is ON by default except if VERBOSE=1 option is given to make
 
 SHOW := $(if $(VERBOSE),@true "",@echo "")
@@ -231,7 +231,7 @@ grammar/grammar.cma : $(GRAMCMO)
 	$(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl test.mlp -o test.ml
 	$(HIDE)$(GRAMC) test.ml -o test-grammar
 	@rm -f test-grammar test.*
-	$(SHOW)'OCAMLC -a $@'   
+	$(SHOW)'OCAMLC -a $@'
 	$(HIDE)$(GRAMC) $^ -linkall -a -o $@
 
 ## Support of Camlp5 and Camlp5
@@ -283,7 +283,7 @@ minibyte: $(COQTOPBYTE) pluginsbyte
 
 ifeq ($(BEST),opt)
 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
-	$(SHOW)'COQMKTOP -o $@'	
+	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@
 	$(STRIP) $@
 	$(CODESIGN) $@
@@ -293,7 +293,7 @@ $(COQTOPEXE): $(COQTOPBYTE)
 endif
 
 $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA)
-	$(SHOW)'COQMKTOP -o $@'	
+	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@
 
 LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) )
@@ -896,7 +896,7 @@ install-emacs:
 
 install-latex:
 	$(MKDIR) $(FULLCOQDOCDIR)
-	$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)	
+	$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
 #	-$(UPDATETEX)
 
 ###########################################################################
@@ -968,7 +968,7 @@ dev/printers.cma: dev/printers.mllib
 	$(SHOW)'Testing $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer
 	@rm -f test-printer
-	$(SHOW)'OCAMLC -a $@'   
+	$(SHOW)'OCAMLC -a $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@
 
 ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
@@ -1107,7 +1107,7 @@ plugins/%_mod.ml: plugins/%.mllib
 
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP)
 	$(SHOW)'COQC      $<'
-	$(HIDE)rm -f $*.glob 
+	$(HIDE)rm -f $*.glob
 	$(HIDE)$(BOOTCOQC) $<
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
@@ -1187,7 +1187,7 @@ otags:
 Makefile Makefile.build Makefile.common config/Makefile : ;
 
 
-# For emacs: 
-# Local Variables: 
-# mode: makefile 
+# For emacs:
+# Local Variables:
+# mode: makefile
 # End:
diff --git a/Makefile.common b/Makefile.common
index 86a7ea847..f592cd6ec 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -12,7 +12,7 @@
 # Executables
 ###########################################################################
 
-COQMKTOP:=bin/coqmktop$(EXE) 
+COQMKTOP:=bin/coqmktop$(EXE)
 
 COQC:=bin/coqc$(EXE)
 
@@ -35,7 +35,7 @@ else
 endif
 
 INSTALLBIN:=install
-INSTALLLIB:=install -m 644 
+INSTALLLIB:=install -m 644
 INSTALLSH:=./install.sh
 MKDIR:=install -d
 
@@ -119,7 +119,7 @@ HTMLSTYLE:=simple
 export TEXINPUTS:=$(HEVEALIB):
 COQTEXOPTS:=-boot -n 72 -sl -small
 
-DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex 
+DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 
 REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex RefMan-ext.v.tex \
@@ -149,7 +149,7 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
 
 
 ###########################################################################
-# Object and Source files 
+# Object and Source files
 ###########################################################################
 
 COQRUN := coqrun
@@ -393,7 +393,7 @@ GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
 GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
 
 
-# For emacs: 
-# Local Variables: 
-# mode: makefile 
+# For emacs:
+# Local Variables:
+# mode: makefile
 # End:
diff --git a/lib/pp.ml b/lib/pp.ml
index d07f01b90..99c774e8d 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -44,7 +44,7 @@ end
 
 module Tag :
 sig
-  type t 
+  type t
   type 'a key
   val create : string -> 'a key
   val inj : 'a -> 'a key -> t
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5ee9b0fc4..2c1f59634 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -988,7 +988,7 @@ let interp_bindings ist env sigma = function
 | NoBindings ->
     sigma, NoBindings
 | ImplicitBindings l ->
-    let sigma, l = interp_open_constr_list ist env sigma l in   
+    let sigma, l = interp_open_constr_list ist env sigma l in
     sigma, ImplicitBindings l
 | ExplicitBindings l ->
     let sigma, l = List.fold_map (interp_binding ist env) sigma l in
@@ -1164,7 +1164,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
         in
 	Tactic_debug.debug_prompt lev tac eval
   | _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
-      
+
 
 and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacAtom (loc,t) ->
@@ -1309,7 +1309,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t =
   | ArgArg (loc,r) ->
       let ids = extract_ids [] ist.lfun in
       let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in
-      let extra = TacStore.set ist.extra f_avoid_ids ids in 
+      let extra = TacStore.set ist.extra f_avoid_ids ids in
       let extra = TacStore.set extra f_trace (push_trace loc_info ist) in
       let ist = { lfun = Id.Map.empty; extra = extra; } in
       let appl = GlbAppl[r,[]] in
@@ -1633,7 +1633,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
-        Tacticals.New.tclWITHHOLES false 
+        Tacticals.New.tclWITHHOLES false
         (name_atomic ~env
           (TacIntroPattern l)
           (* spiwack: print uninterpreted, not sure if it is the
@@ -1648,7 +1648,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma = project gl in
 	let l = List.map (fun (k,c) ->
           let loc, f = interp_open_constr_with_bindings_loc ist c in
-	    (k,(loc,f))) cb 
+	    (k,(loc,f))) cb
 	in
         let sigma,tac = match cl with
           | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
@@ -1661,7 +1661,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacElim (ev,(keep,cb),cbo) ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
-        let sigma = project gl in 
+        let sigma = project gl in
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
         let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
         let named_tac =
@@ -1715,7 +1715,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
-        let (sigma,c) = 
+        let (sigma,c) =
           (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
         in
         let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in
@@ -1825,7 +1825,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let c_interp patvars = { Sigma.run = begin fun sigma ->
 	  let lfun' = Id.Map.fold (fun id c lfun ->
-	    Id.Map.add id (Value.of_constr c) lfun) 
+	    Id.Map.add id (Value.of_constr c) lfun)
 	    patvars ist.lfun
 	  in
 	  let sigma = Sigma.to_evar_map sigma in
@@ -1851,7 +1851,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
         let c_interp patvars = { Sigma.run = begin fun sigma ->
           let lfun' = Id.Map.fold (fun id c lfun ->
-            Id.Map.add id (Value.of_constr c) lfun) 
+            Id.Map.add id (Value.of_constr c) lfun)
             patvars ist.lfun
           in
           let ist = { ist with lfun = lfun' } in