aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/gallina.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/gallina.ml')
-rw-r--r--tools/gallina.ml22
1 files changed, 11 insertions, 11 deletions
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 8b3944207..8ba9ae104 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -16,29 +16,29 @@ let option_moins = ref false
let option_stdout = ref false
-let traite_fichier f =
- try
- let chan_in = open_in (f^".v") in
+let traite_fichier f =
+ try
+ let chan_in = open_in (f^".v") in
let buf = Lexing.from_channel chan_in in
if not !option_stdout then chan_out := open_out (f ^ ".g");
- try
+ try
while true do Gallina_lexer.action buf done
- with Fin_fichier -> begin
+ with Fin_fichier -> begin
flush !chan_out;
close_in chan_in;
if not !option_stdout then close_out !chan_out
end
- with Sys_error _ ->
- ()
+ with Sys_error _ ->
+ ()
let traite_stdin () =
try
let buf = Lexing.from_channel stdin in
- try
+ try
while true do Gallina_lexer.action buf done
- with Fin_fichier ->
+ with Fin_fichier ->
flush !chan_out
- with Sys_error _ ->
+ with Sys_error _ ->
()
let gallina () =
@@ -52,7 +52,7 @@ let gallina () =
| "-" -> option_moins := true
| "-stdout" -> option_stdout := true
| "-nocomments" -> comments := false
- | f ->
+ | f ->
if Filename.check_suffix f ".v" then
vfiles := (Filename.chop_suffix f ".v") :: !vfiles
in