From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 17 Sep 2009 15:58:14 +0000
Subject: 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
---
 plugins/syntax/string_syntax.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/syntax/string_syntax.ml')

diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index d1c263dc8c..bc02357aea 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -38,14 +38,14 @@ open Lazy
 
 let interp_string dloc s =
   let le = String.length s in
-  let rec aux n = 
+  let rec aux n =
      if n = le then RRef (dloc, force glob_EmptyString) else
      RApp (dloc,RRef (dloc, force glob_String),
        [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
 let uninterp_string r =
-  try 
+  try
     let b = Buffer.create 16 in
     let rec aux = function
     | RApp (_,RRef (_,k),[a;s]) when k = force glob_String ->
@@ -57,13 +57,13 @@ let uninterp_string r =
     | _ ->
 	raise Non_closed_string
     in aux r
-  with 
+  with
    Non_closed_string -> None
 
 let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([RRef (dummy_loc,static_glob_String); 
+    ([RRef (dummy_loc,static_glob_String);
       RRef (dummy_loc,static_glob_EmptyString)],
      uninterp_string, true)
-- 
cgit v1.2.3