aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_lexer.mll
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /tools/coqdep_lexer.mll
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
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
Diffstat (limited to 'tools/coqdep_lexer.mll')
-rwxr-xr-xtools/coqdep_lexer.mll32
1 files changed, 16 insertions, 16 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 3c7d09e1f..b13c16bad 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -7,26 +7,26 @@
(************************************************************************)
(*i $Id$ i*)
-
+
{
- open Filename
+ open Filename
open Lexing
-
+
type mL_token = Use_module of string
type spec = bool
-
- type coq_token =
+
+ type coq_token =
| Require of string list list
| RequireString of string
| Declare of string list
| Load of string
let comment_depth = ref 0
-
+
exception Fin_fichier
-
+
let module_current_name = ref []
let module_names = ref []
let ml_module_name = ref ""
@@ -62,10 +62,10 @@ rule coq_action = parse
| "\""
{ string lexbuf; coq_action lexbuf}
| "(*" (* "*)" *)
- { comment_depth := 1; comment lexbuf; coq_action lexbuf }
- | eof
- { raise Fin_fichier}
- | _
+ { comment_depth := 1; comment lexbuf; coq_action lexbuf }
+ | eof
+ { raise Fin_fichier}
+ | _
{ coq_action lexbuf }
and caml_action = parse
@@ -132,7 +132,7 @@ and comment = parse
| "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
{ comment lexbuf }
| eof
- { raise Fin_fichier }
+ { raise Fin_fichier }
| _ { comment lexbuf }
and string = parse
@@ -157,7 +157,7 @@ and load_file = parse
Load (if check_suffix f ".v" then chop_suffix f ".v" else f) }
| coq_ident
{ let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
- | eof
+ | eof
{ raise Fin_fichier }
| _
{ load_file lexbuf }
@@ -196,7 +196,7 @@ and opened_file_fields = parse
{ module_current_name :=
field_name (Lexing.lexeme lexbuf) :: !module_current_name;
opened_file_fields lexbuf }
- | coq_ident { module_names :=
+ | coq_ident { module_names :=
List.rev !module_current_name :: !module_names;
module_current_name := [Lexing.lexeme lexbuf];
opened_file_fields lexbuf }
@@ -211,10 +211,10 @@ and modules = parse
| "(*" (* "*)" *) { comment_depth := 1; comment lexbuf;
modules lexbuf }
| '"' [^'"']* '"'
- { let lex = (Lexing.lexeme lexbuf) in
+ { let lex = (Lexing.lexeme lexbuf) in
let str = String.sub lex 1 (String.length lex - 2) in
mllist := str :: !mllist; modules lexbuf}
- | _ { (Declare (List.rev !mllist)) }
+ | _ { (Declare (List.rev !mllist)) }
and qual_id = parse
| '.' [^ '.' '(' '['] {