Clean trailing whitespace

5 files changed, 149 insertions, 149 deletions

diff --git a/src/lexer.mll b/src/lexer.mll
index df5725aa..8d2be0d3 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -53,7 +53,7 @@ let r = fun s -> s (* Ulib.Text.of_latin1 *)
 (* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
 let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
 
-let kw_table = 
+let kw_table =
   List.fold_left
     (fun r (x,y) -> M.add x y r)
     M.empty
@@ -74,7 +74,7 @@ let kw_table =
      ("function",                (fun x -> Function_(x)));
      ("if",                      (fun x -> If_(x)));
      ("in",			 (fun x -> In(x)));
-     ("IN",                      (fun x -> IN(x)));     
+     ("IN",                      (fun x -> IN(x)));
      ("let",                     (fun x -> Let_(x)));
      ("member",                  (fun x -> Member(x)));
      ("Nat",                     (fun x -> Nat(x)));
@@ -124,8 +124,8 @@ rule token skips = parse
     { token (Parse_ast.Ws(r i)::skips) lexbuf }
   | "\n"
     { Lexing.new_line lexbuf;
-      token (Parse_ast.Nl::skips) lexbuf } 
-  
+      token (Parse_ast.Nl::skips) lexbuf }
+
   | "&"					{ (Amp(Some(skips),r"&")) }
   | "@"					{ (At(Some(skips),r"@")) }
   | "|"                                 { (Bar(Some(skips))) }
@@ -156,7 +156,7 @@ rule token skips = parse
   | "|]"				{ (BarSquare(Some(skips))) }
   | "^^"				{ (CarrotCarrot(Some(skips),r"^^")) }
   | "::" as i                           { (ColonColon(Some(skips),r i)) }
-  | ".."				{ (DotDot(Some(skips))) }  
+  | ".."				{ (DotDot(Some(skips))) }
   | "=/="				{ (EqDivEq(Some(skips),r"=/=")) }
   | "=="				{ (EqEq(Some(skips),r"==")) }
   | "!="				{ (ExclEq(Some(skips),r"!=")) }
@@ -202,7 +202,7 @@ rule token skips = parse
   | "2^"				{ (TwoCarrot(Some(skips),r"2^")) }
 
 
-  | "--"                           
+  | "--"
     { token (Parse_ast.Com(Parse_ast.Comment(comment lexbuf))::skips) lexbuf }
 
   | startident ident* as i              { if M.mem i kw_table then
@@ -264,7 +264,7 @@ rule token skips = parse
   | "*_u" oper_char+ as i				{ (StarUnderUI(Some(skips),r i)) }
   | "*_ui" oper_char+ as i				{ (StarUnderUiI(Some(skips),r i)) }
   | "2^" oper_char+ as i				{ (TwoCarrotI(Some(skips),r i)) }
-  
+
   | digit+ as i                         { (Num(Some(skips),int_of_string i)) }
   | "0b" (binarydigit+ as i)		{ (Bin(Some(skips), i)) }
   | "0x" (hexdigit+ as i) 		{ (Hex(Some(skips), i)) }
diff --git a/src/main.ml b/src/main.ml
index 2f256cb2..f790627c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -60,22 +60,22 @@ let isa_theory = ref None
 let opt_file_arguments = ref ([]:string list)
 
 let options = Arg.align ([
-  ( "-i", 
+  ( "-i",
     Arg.String (fun l -> lib := l::!lib),
     " treat the file as input only and generate no output for it");
-  ( "-tex", 
+  ( "-tex",
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then
                 backends := Some(Typed_ast.Target_tex)::!backends),
     " generate LaTeX");
-  ( "-html", 
+  ( "-html",
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then
                 backends := Some(Typed_ast.Target_html)::!backends),
     " generate Html");
-  ( "-hol", 
+  ( "-hol",
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then
                 backends := Some(Typed_ast.Target_hol)::!backends),
     " generate HOL");
-  ( "-ocaml", 
+  ( "-ocaml",
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then
                 backends := Some(Typed_ast.Target_ocaml)::!backends),
     " generate OCaml");
@@ -94,22 +94,22 @@ let options = Arg.align ([
   ( "-print_types",
     Arg.Unit (fun b -> opt_print_types := true),
     " print types on stdout");
-  ( "-lib", 
+  ( "-lib",
     Arg.String (fun l -> opt_library := Some l),
     " library path"^match !opt_library with None->"" | Some s -> " (default "^s^")");
-  ( "-ocaml_lib", 
+  ( "-ocaml_lib",
     Arg.String (fun l -> ocaml_lib := l::!ocaml_lib),
     " add to OCaml library");
-  ( "-hol_lib", 
+  ( "-hol_lib",
     Arg.String (fun l -> hol_lib := l::!hol_lib),
     " add to HOL library");
-  ( "-isa_lib", 
+  ( "-isa_lib",
     Arg.String (fun l -> isa_lib := l::!isa_lib),
     " add to Isabelle library");
-  ( "-isa_theory", 
+  ( "-isa_theory",
     Arg.String (fun l -> isa_theory := Some l),
     " Isabelle Lem theory");
-  ( "-coq_lib", 
+  ( "-coq_lib",
     Arg.String (fun l -> coq_lib := l::!coq_lib),
     " add to Coq library");
   ( "-v",
@@ -121,7 +121,7 @@ let options = Arg.align ([
   ( "-only_changed_output",
     Arg.Unit (fun b -> Process_file.always_replace_files := false),
     " generate only output files, whose content really changed compared to the existing file");
-  ( "-extra_level", 
+  ( "-extra_level",
     Arg.Symbol (["none"; "auto"; "all"], (fun s ->
      Backend.gen_extra_level := (match s with
        | "none" -> 0
@@ -130,14 +130,14 @@ let options = Arg.align ([
     " generate no (none) extra-information, only extras that can be handled automatically (auto) or all (all) extra information")
 ] @ Reporting.warn_opts)
 
-let usage_msg = 
+let usage_msg =
     ("Lem " ^ Version.v ^ "\n"
-     ^ "example usage:       lem -hol -ocaml -lib ../lem/library test.lem\n" 
+     ^ "example usage:       lem -hol -ocaml -lib ../lem/library test.lem\n"
     )
 
-let _ = 
-  Arg.parse options 
-    (fun s -> 
+let _ =
+  Arg.parse options
+    (fun s ->
       opt_file_arguments := (!opt_file_arguments) @ [s])
     usage_msg
 
@@ -177,14 +177,14 @@ let per_target libpath isa_thy modules (def_info,env) consts alldoc_accum alldoc
   let module T = Target_trans.Make(C) in
   let (trans,avoid) = T.get_transformation targ consts in
     try
-      let (_,transformed_m) = 
-        List.fold_left 
-          (fun (env,new_mods) old_mod -> 
+      let (_,transformed_m) =
+        List.fold_left
+          (fun (env,new_mods) old_mod ->
              let (env,m) = trans env old_mod in
                (env,m::new_mods))
           (env,[])
           modules
-      in      
+      in
       let consts' = T.extend_consts targ consts transformed_m in
       let transformed_m' = T.rename_def_params targ consts' transformed_m in
         output libpath isa_thy targ (avoid consts') def_info (List.rev transformed_m') alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum
@@ -199,38 +199,38 @@ let per_target libpath isa_thy modules (def_info,env) consts alldoc_accum alldoc
 
 let main () =
   let _ = if !opt_print_version then print_string ("Lem " ^ Version.v ^ "\n") in
-  let lib_path = 
+  let lib_path =
     match !opt_library with
-      | None -> (try 
+      | None -> (try
                 let lp = Sys.getenv("LEMLIB") in
-                if Filename.is_relative lp 
+                if Filename.is_relative lp
                 then Filename.concat (Sys.getcwd ()) lp
                 else lp
-            with 
+            with
                 | Not_found -> raise (Failure("must specify a -lib argument or have a LEMLIB environment variable")))
-      | Some lp -> 
+      | Some lp ->
           if Filename.is_relative lp then
             Filename.concat (Sys.getcwd ()) lp
           else
             lp
   in
-  let isa_thy = 
+  let isa_thy =
     match !isa_theory with
       | None -> Filename.concat lib_path "../isabelle-lib/Lem"
       | Some thy -> thy
   in
-  let _ = 
+  let _ =
     List.iter
       (fun f ->
          try
            if String.compare ".lem" (String.sub f (String.length f - 4) 4) <> 0 then
              raise (Failure("Files must have .lem extension"))
-         with 
-           | Invalid_argument _ -> 
+         with
+           | Invalid_argument _ ->
              raise (Failure("Files must have .lem extension")))
       (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib)
   in
-  let _ = 
+  let _ =
     List.iter
       (fun f ->
          if not (Str.string_match (Str.regexp "[A-Za-z]") (Filename.basename f) 0) then
@@ -257,9 +257,9 @@ let main () =
   let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_isa) !isa_lib init in
   let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_coq) !coq_lib init in
 
-  let consts = 
+  let consts =
     List.map
-      (fun (targ,cL) ->        
+      (fun (targ,cL) ->
         let consts = List.fold_left
               (fun s c -> Typed_ast.NameSet.add (Name.from_rope c) s)
               Typed_ast.NameSet.empty
@@ -276,8 +276,8 @@ let main () =
          let f' = Filename.basename (Filename.chop_extension f) in
          let mod_name = String.capitalize f' in
          let mod_name_name = Name.from_rope (Ulib.Text.of_latin1 mod_name) in
-         let backend_set = 
-           List.fold_right 
+         let backend_set =
+           List.fold_right
              (fun x s ->
                 match x with
                   | None -> s
@@ -285,14 +285,14 @@ let main () =
                   | Some(Typed_ast.Target_html) -> s
                   | Some(t) -> Typed_ast.Targetset.add t s)
              !backends
-             Typed_ast.Targetset.empty 
+             Typed_ast.Targetset.empty
          in
-         let ((tdefs,instances,new_instances),new_env,tast) = 
+         let ((tdefs,instances,new_instances),new_env,tast) =
            check_ast backend_set [mod_name_name] (def_info,env) ast
          in
          let md = { Typed_ast.mod_env = new_env; Typed_ast.mod_binding = Path.mk_path [] mod_name_name } in
          let e = { env with Typed_ast.m_env = Typed_ast.Nfmap.insert env.Typed_ast.m_env (mod_name_name,md) } in
-         let module_record = 
+         let module_record =
            { Typed_ast.filename = f;
              Typed_ast.module_name = mod_name;
              Typed_ast.predecessor_modules = previously_processed_modules;
@@ -314,12 +314,12 @@ let main () =
            ((if add_to_modules then
              module_record::mods
                else
-             mods), 
+             mods),
             ((tdefs,instances),e), mod_name::previously_processed_modules))
       ([],type_info,[])
       (* We don't want to add the files in !lib to the resulting module ASTs,
        * because we don't want to put them throught the back end *)
-      (List.map (fun x -> (x, false)) (List.rev !lib) @ 
+      (List.map (fun x -> (x, false)) (List.rev !lib) @
        List.map (fun x -> (x, true)) !opt_file_arguments)
   in
 
@@ -332,13 +332,13 @@ let main () =
   let alldoc_inc_accum = ref ([] : Ulib.Text.t list) in
   let alldoc_inc_usage_accum = ref ([] : Ulib.Text.t list) in
     ignore (List.iter (per_target lib_path isa_thy (List.rev modules) type_info consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) !backends);
-    (if List.mem (Some(Typed_ast.Target_tex)) !backends then 
+    (if List.mem (Some(Typed_ast.Target_tex)) !backends then
        output_alldoc "alldoc" (String.concat " " !opt_file_arguments) alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum)
 
-let _ = 
-  try 
+let _ =
+  try
     begin
-      try ignore(main ()) 
+      try ignore(main ())
       with  Failure(s) -> raise (Reporting_basic.err_general false Ast.Unknown ("Failure "^s))
     end
   with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e
@@ -349,22 +349,22 @@ let lib = ref []
 let opt_print_version = ref false
 let opt_file_arguments = ref ([]:string list)
 let options = Arg.align ([
-  ( "-i", 
+  ( "-i",
     Arg.String (fun l -> lib := l::!lib),
     " treat the file as input only and generate no output for it");
-  (*( "-tex", 
+  (*( "-tex",
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then
                 backends := Some(Typed_ast.Target_tex)::!backends),
     " generate LaTeX");
-  ( "-html", 
+  ( "-html",
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then
                 backends := Some(Typed_ast.Target_html)::!backends),
     " generate Html");
-  ( "-hol", 
+  ( "-hol",
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then
                 backends := Some(Typed_ast.Target_hol)::!backends),
     " generate HOL");
-  ( "-ocaml", 
+  ( "-ocaml",
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then
                 backends := Some(Typed_ast.Target_ocaml)::!backends),
     " generate OCaml");
@@ -388,14 +388,14 @@ let options = Arg.align ([
     " print version");
 ] )
 
-let usage_msg = 
+let usage_msg =
     ("L2 " ^ "pre alpha" ^ "\n"
-     ^ "example usage:       l2 test.ltwo\n" 
+     ^ "example usage:       l2 test.ltwo\n"
     )
 
-let _ = 
-  Arg.parse options 
-    (fun s -> 
+let _ =
+  Arg.parse options
+    (fun s ->
       opt_file_arguments := (!opt_file_arguments) @ [s])
     usage_msg
 
diff --git a/src/parser.mly b/src/parser.mly
index b9aedb65..19e66747 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -107,8 +107,8 @@ let star = "*"
 (*let mk_pre_x_l sk1 (sk2,id) sk3 l =
   if (sk2 = None || sk2 = Some []) && (sk3 = None || sk3 = Some []) then
     PreX_l(sk1,(None,id),None,l)
-  else if (sk2 = Some [Ws space] && 
-           sk3 = Some [Ws space] && 
+  else if (sk2 = Some [Ws space] &&
+           sk3 = Some [Ws space] &&
            (Ulib.Text.left id 1 = star ||
             Ulib.Text.right id 1 = star)) then
     PreX_l(sk1,(None,id),None,l)
@@ -120,15 +120,15 @@ let star = "*"
 
 /*Terminals with no content*/
 
-%token <Parse_ast.terminal> And As Bits Case Clause Const Default Effect Effects End Enum Else False 
-%token <Parse_ast.terminal> Forall Function_ If_ In IN Let_ Member Nat Order Pure Rec Register  
+%token <Parse_ast.terminal> And As Bits Case Clause Const Default Effect Effects End Enum Else False
+%token <Parse_ast.terminal> Forall Function_ If_ In IN Let_ Member Nat Order Pure Rec Register
 %token <Parse_ast.terminal> Scattered Struct Switch Then True Type TYPE Typedef Union With Val
 
-%token <Parse_ast.terminal> AND Div_ EOR Mod OR Quot Rem 
+%token <Parse_ast.terminal> AND Div_ EOR Mod OR Quot Rem
 
 %token <Parse_ast.terminal> Bar Colon Comma Dot Eof Minus Semi Under
 %token <Parse_ast.terminal> Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token <Parse_ast.terminal> BarBar BarGt BarSquare DotDot MinusGt LtBar SquareBar 
+%token <Parse_ast.terminal> BarBar BarGt BarSquare DotDot MinusGt LtBar SquareBar
 
 /*Terminals with content*/
 
@@ -136,24 +136,24 @@ let star = "*"
 %token <Parse_ast.terminal * int> Num
 %token <Parse_ast.terminal * string> String Bin Hex
 
-%token <Parse_ast.terminal * string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde 
-%token <Parse_ast.terminal * string> AmpAmp CarrotCarrot ColonColon ColonEq EqDivEq EqEq ExclEq ExclExcl  
-%token <Parse_ast.terminal * string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt   
+%token <Parse_ast.terminal * string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde
+%token <Parse_ast.terminal * string> AmpAmp CarrotCarrot ColonColon ColonEq EqDivEq EqEq ExclEq ExclExcl
+%token <Parse_ast.terminal * string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
 %token <Parse_ast.terminal * string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
 
-%token <Parse_ast.terminal * string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS 
-%token <Parse_ast.terminal * string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU 
-%token <Parse_ast.terminal * string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS 
+%token <Parse_ast.terminal * string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
+%token <Parse_ast.terminal * string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
+%token <Parse_ast.terminal * string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
 %token <Parse_ast.terminal * string> StarUnderSi StarUnderU StarUnderUi TwoCarrot
 
 %token <Parse_ast.terminal * string> AmpI AtI CarrotI  DivI EqI ExclI GtI LtI PlusI StarI TildeI
-%token <Parse_ast.terminal * string> AmpAmpI CarrotCarrotI ColonColonI ColonEqI EqDivEqI EqEqI ExclEqI ExclExclI  
-%token <Parse_ast.terminal * string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI  
+%token <Parse_ast.terminal * string> AmpAmpI CarrotCarrotI ColonColonI ColonEqI EqDivEqI EqEqI ExclEqI ExclExclI
+%token <Parse_ast.terminal * string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI
 %token <Parse_ast.terminal * string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
 
-%token <Parse_ast.terminal * string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI 
-%token <Parse_ast.terminal * string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI 
-%token <Parse_ast.terminal * string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI 
+%token <Parse_ast.terminal * string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI
+%token <Parse_ast.terminal * string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI
+%token <Parse_ast.terminal * string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI
 %token <Parse_ast.terminal * string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
 
 %start file
@@ -264,19 +264,19 @@ atomic_typs:
   | atomic_typ
     { [$1] }
   | atomic_typ atomic_typs
-    { $1::$2 } 
+    { $1::$2 }
 
 app_typ:
   | vtyp_typ
     { $1 }
   | id atomic_typs
-    { tloc (ATyp_app($1,$2)) } 
+    { tloc (ATyp_app($1,$2)) }
 
 star_typ_list:
   | app_typ
     { [($1,None)] }
   | app_typ Star star_typ_list
-    { ($1,fst $2)::$3 } 
+    { ($1,fst $2)::$3 }
 
 star_typ:
   | star_typ_list
@@ -292,19 +292,19 @@ exp_typ:
    | Num StarStar typ
      { if (2 = (snd $1))
        then tloc (ATyp_exp((fst $1),(fst $2),$3))
-       else raise (Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats")) } 
+       else raise (Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats")) }
 
 nexp_typ:
    | exp_typ
      { $1 }
    | atomic_typ Plus typ
-     { tloc (ATyp_sum($1,fst $2,$3)) } 
+     { tloc (ATyp_sum($1,fst $2,$3)) }
 
 typ:
   | nexp_typ
     { $1 }
   | star_typ MinusGt atomic_typ effect_typ
-    { tloc (ATyp_fn($1,$2,$3,$4)) } 
+    { tloc (ATyp_fn($1,$2,$3,$4)) }
 
 lit:
   | True
@@ -334,7 +334,7 @@ atomic_pat:
 /*  | Lparen atomic_typ pat Rparen
     { ploc (P_typ($1,$2,$3,$4)) } */
   | id
-    { ploc (P_app($1,[])) } 
+    { ploc (P_app($1,[])) }
   | Lcurly fpats Rcurly
     { ploc (P_record($1,fst $2,fst (snd $2),snd (snd $2),$3)) }
   | Lsquare pat Rsquare
@@ -342,11 +342,11 @@ atomic_pat:
   | Lsquare comma_pats Rsquare
     { ploc (P_vector($1,$2,$3)) }
   | Lsquare npats Rsquare
-    { ploc (P_vector_indexed($1,$2,$3)) } 
+    { ploc (P_vector_indexed($1,$2,$3)) }
   | Lparen comma_pats Rparen
-    { ploc (P_tup($1,$2,$3)) } 
+    { ploc (P_tup($1,$2,$3)) }
   | SquareBar comma_pats BarSquare
-    { ploc (P_list($1,$2,$3)) } 
+    { ploc (P_list($1,$2,$3)) }
   | Lparen pat Rparen
     { $2 }
 
@@ -366,7 +366,7 @@ pat:
   | app_pat
     { $1 }
   | pat_colons
-    { ploc (P_vector_concat($1)) } 
+    { ploc (P_vector_concat($1)) }
 
 comma_pats:
   | atomic_pat Comma atomic_pat
@@ -386,7 +386,7 @@ fpats:
   | fpat Semi fpats
     { (($1,$2)::fst $3, snd $3) }
 
-npat: 
+npat:
   | Num Eq pat
     { ($1,fst $2,$3) }
 
@@ -399,8 +399,8 @@ npats:
 atomic_exp:
   | Lcurly semi_exps Rcurly
     { eloc (E_block($1,$2,$3)) }
-  | id 
-    { eloc (E_id($1)) } 
+  | id
+    { eloc (E_id($1)) }
   | lit
     { eloc (E_lit($1)) }
   | Lparen exp Rparen
@@ -444,7 +444,7 @@ right_atomic_exp:
   | If_ exp Then exp Else exp
     { eloc (E_if($1,$2,$3,$4,$5,$6)) }
   | letbind In exp
-    { eloc (E_let($1,$2,$3)) } 
+    { eloc (E_let($1,$2,$3)) }
 
 starstar_exp:
   | app_exp
@@ -524,7 +524,7 @@ eq_right_atomic_exp:
     { $1 }
   | eq_exp Eq at_right_atomic_exp
     { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp ColonEq at_right_atomic_exp 
+  | eq_exp ColonEq at_right_atomic_exp
     { eloc (E_assign($1,fst $2,$3)) }
 
 and_exp:
@@ -554,7 +554,7 @@ or_right_atomic_exp:
 
 exp:
   | or_exp
-    { $1 } 
+    { $1 }
   | or_right_atomic_exp
     { $1 }
 
@@ -564,7 +564,7 @@ comma_exps:
     { [($1,$2);($3,None)] }
   | exp Comma comma_exps
     { ($1,$2)::$3 }
- 
+
 semi_exps_help:
   | exp
     { [($1,None)] }
@@ -598,11 +598,11 @@ letbind:
     { lbloc (LB_val_implicit($1,$2,fst $3,$4)) }
   | Let_ typquant atomic_typ atomic_pat Eq exp
     { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,fst $5,$6)) }
-  /* This is ambiguous causing 4 shift/reduce and 5 reduce/reduce conflicts because the parser can't tell until the end of typ whether it was parsing a type or a pattern, and this seem to be too late. Solutions are to have a different keyword for this and the above solution besides let (while still absolutely having a keyword here) 
+  /* This is ambiguous causing 4 shift/reduce and 5 reduce/reduce conflicts because the parser can't tell until the end of typ whether it was parsing a type or a pattern, and this seem to be too late. Solutions are to have a different keyword for this and the above solution besides let (while still absolutely having a keyword here)
   | Let_ atomic_typ atomic_pat Eq exp
     { } */
 
-funcl: 
+funcl:
   | id atomic_pat Eq exp
     { funclloc (FCL_Funcl($1,$2,fst $3,$4)) }
 
@@ -617,26 +617,26 @@ fun_def:
   | Function_ Rec typquant atomic_typ effect_typ funcl_ands
     { funloc (FD_function($1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
   | Function_ Rec typquant atomic_typ funcl_ands
-    { funloc (FD_function($1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }  
+    { funloc (FD_function($1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
   | Function_ Rec atomic_typ effect_typ funcl_ands
     { funloc (FD_function($1,mk_rec $2 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
   | Function_ Rec atomic_typ funcl_ands
     { match $3 with
-      | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) -> 
+      | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) ->
         funloc (FD_function($1,mk_rec $2 2,mk_tannotn (), mk_eannot $3 3, $4))
-      | _ -> 
+      | _ ->
         funloc (FD_function($1,mk_rec $2 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
   | Function_ Rec funcl_ands
     { funloc (FD_function($1,mk_rec $2 2, mk_tannotn (), mk_eannotn (), $3)) }
   | Function_ typquant atomic_typ effect_typ funcl_ands
     { funloc (FD_function($1,mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
   | Function_ typquant atomic_typ funcl_ands
-    { funloc (FD_function($1,mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }  
+    { funloc (FD_function($1,mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }
   | Function_ atomic_typ funcl_ands
     { match $2 with
-      | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) -> 
+      | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) ->
         funloc (FD_function($1,mk_recn (),mk_tannotn (), mk_eannot $2 2, $3))
-      | _ -> 
+      | _ ->
         funloc (FD_function($1,mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
   | Function_ funcl_ands
     { funloc (FD_function($1,mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
@@ -676,12 +676,12 @@ nexp_constraint:
   | typ LtEq typ
     { NC_aux(NC_bounded_le($1,(fst $2),$3), loc () ) }
   | id IN Lcurly nums Rcurly
-    { NC_aux(NC_nat_set_bounded($1,$2,$3,$4,$5), loc ()) } 
-    
+    { NC_aux(NC_nat_set_bounded($1,$2,$3,$4,$5), loc ()) }
+
 nexp_constraints:
   | nexp_constraint
     { [($1,None)] }
-  | nexp_constraint Comma nexp_constraints 
+  | nexp_constraint Comma nexp_constraints
     { ($1,$2)::$3 }
 
 typquant:
@@ -701,7 +701,7 @@ c_def_body:
   | typ id Semi
     { [(($1,$2),None)],($3,true) }
   | typ id Semi c_def_body
-    { (($1,$2),$3)::(fst $4), snd $4 } 
+    { (($1,$2),$3)::(fst $4), snd $4 }
 
 index_range_atomic:
   | Num
@@ -715,7 +715,7 @@ index_range:
   | index_range_atomic
     { $1 }
   | index_range_atomic Comma index_range
-    { irloc(BF_concat($1,$2,$3)) } 
+    { irloc(BF_concat($1,$2,$3)) }
 
 r_id_def:
   | index_range Colon id
@@ -761,12 +761,12 @@ type_def:
 
 default_typ:
   | Default atomic_kind id
-    { defloc (DT_kind($1,$2,$3)) } 
+    { defloc (DT_kind($1,$2,$3)) }
   | Default typquant atomic_typ id
     { defloc (DT_typ($1,(mk_typschm $2 $3 2 3),$4)) }
   | Default atomic_typ id
     { defloc (DT_typ($1,(mk_typschm (mk_typqn ()) $2 2 2),$3)) }
- 
+
 scattered_def:
   | Function_ Rec typquant atomic_typ effect_typ id
     { (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
@@ -776,7 +776,7 @@ scattered_def:
     { (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
   | Function_ Rec atomic_typ id
     { match $3 with
-      | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) -> 
+      | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) ->
         (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannotn (), mk_eannot $3 3, $4))
       | _ ->
         (DEF_scattered_function(None,$1,mk_rec $2 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
@@ -790,7 +790,7 @@ scattered_def:
     { (DEF_scattered_function(None,$1,mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
   | Function_ atomic_typ id
     { match $2 with
-      | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) -> 
+      | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) ->
         (DEF_scattered_function(None,$1,mk_recn (), mk_tannotn (), mk_eannot $2 2, $3))
       | _ ->
         (DEF_scattered_function(None,$1,mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
@@ -814,7 +814,7 @@ def:
     { dloc (DEF_val($1)) }
   | val_spec
     { dloc (DEF_spec($1)) }
-  | default_typ 
+  | default_typ
     { dloc (DEF_default($1)) }
   | Register atomic_typ id
     { dloc (DEF_reg_dec($1,$2,$3)) }
@@ -827,7 +827,7 @@ def:
     { dloc (DEF_scattered_funcl($1,$2,$3)) }
   | Union id Member atomic_typ id
     { dloc (DEF_scattered_unioncl($1,$2,$3,$4,$5)) }
-  | End id 
+  | End id
     { dloc (DEF_scattered_end($1,$2)) }
 
 defs_help:
diff --git a/src/process_file.ml b/src/process_file.ml
index fe164957..850a80f2 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -72,13 +72,13 @@ let parse_file (f : string) : (Parse_ast.defs * Parse_ast.lex_skips) =
 
 (* type instances = Types.instance list Types.Pfmap.t
 
-let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list) 
-      ((tdefs,env) : ((Types.type_defs * instances) * Typed_ast.env)) 
+let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list)
+      ((tdefs,env) : ((Types.type_defs * instances) * Typed_ast.env))
       (ast, end_lex_skips)
       : (Types.type_defs * instances * instances) * Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
   try
-    let (defs,env,tast) = 
-      Typecheck.check_defs ts mod_path tdefs env ast 
+    let (defs,env,tast) =
+      Typecheck.check_defs ts mod_path tdefs env ast
     in
       (defs,env,(tast,end_lex_skips))
   with
@@ -86,32 +86,32 @@ let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list)
         raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, m)))
 
 let check_ast_as_module (ts : Typed_ast.Targetset.t) (mod_path : Name.t list)
-      (e : ((Types.type_defs * instances) * Typed_ast.env)) 
+      (e : ((Types.type_defs * instances) * Typed_ast.env))
       (mod_name : Ulib.Text.t) (ast, end_lex_skips)
       : (Types.type_defs * instances * instances) * Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
   check_ast ts mod_path e
-    (Ast.Defs([(Ast.Def_l(Ast.Module(None, Ast.X_l((None,mod_name),Ast.Unknown), None, None, ast, None), Ast.Unknown), 
+    (Ast.Defs([(Ast.Def_l(Ast.Module(None, Ast.X_l((None,mod_name),Ast.Unknown), None, None, ast, None), Ast.Unknown),
                 None,
                 false)]), end_lex_skips)
 
 
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "lem_temp" "" in
-  (o, (o, temp_file_name, file_name)) 
+  (o, (o, temp_file_name, file_name))
 
-let always_replace_files = ref true 
+let always_replace_files = ref true
 
 let close_output_with_check (o, temp_file_name, file_name) =
   let _ = close_out o in
-  let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in 
-  let _ = if (not do_replace) then Sys.remove temp_file_name 
-          else Util.move_file temp_file_name file_name in                   
+  let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in
+  let _ = if (not do_replace) then Sys.remove temp_file_name
+          else Util.move_file temp_file_name file_name in
   ()
 
-let generated_line f = 
+let generated_line f =
   Printf.sprintf "Generated by Lem from %s." f
 
-let tex_preamble = 
+let tex_preamble =
   "\\documentclass{article}\n" ^
   "\\usepackage{amsmath,amssymb}\n" ^
   "\\usepackage{color}\n" ^
@@ -121,12 +121,12 @@ let tex_preamble =
   "\\geometry{a4paper,dvips,twoside,left=22.5mm,right=22.5mm,top=20mm,bottom=30mm}\n" ^
   "\\begin{document}\n"^
   "\\tableofcontents\n\\newpage\n"
-  
-let tex_postamble = 
+
+let tex_postamble =
   "\\end{document}\n"
 
 (* TODO: make this not cppmem-specific *)
-let html_preamble = 
+let html_preamble =
 "\n" ^
 "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n" ^
 "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.1//EN\"\n" ^
@@ -141,7 +141,7 @@ let html_preamble =
 "    <h1 id=\"title\">C/C++ memory model definitions</h1>\n" ^
 "<pre>\n"
 
-let html_postamble = 
+let html_postamble =
 "\n" ^
 "</pre>\n" ^
 "  </body>\n" ^
@@ -159,7 +159,7 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
       | None ->
           let r = B.ident_defs m.typed_ast in
             Printf.printf "%s" (Ulib.Text.to_string r)
-      | Some(Typed_ast.Target_html) -> 
+      | Some(Typed_ast.Target_html) ->
           begin
             let r = B.html_defs m.typed_ast in
             let (o, ext_o) = open_output_with_check (f' ^ ".html") in
@@ -188,7 +188,7 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
                       m.predecessor_modules;
                     Printf.fprintf o "\n\n"
                   end
-                else 
+                else
                   ()
               end
             end in
@@ -211,7 +211,7 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
                 close_output_with_check ext_o
               end in ()
           end
-      | Some(Typed_ast.Target_tex) -> 
+      | Some(Typed_ast.Target_tex) ->
           begin
             let rr = B.tex_defs m.typed_ast in
             (* complete tex document, wrapped in tex_preamble and tex_postamble *)
@@ -239,7 +239,7 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
                     Printf.fprintf o "%s" (Ulib.Text.to_string r_usage);
                     close_output_with_check ext_o
           end
-      | Some(Typed_ast.Target_ocaml) -> 
+      | Some(Typed_ast.Target_ocaml) ->
           begin
             let (r_main, r_extra_opt) = B.ocaml_defs m.typed_ast in
             let _ = begin
@@ -258,21 +258,21 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
                 Printf.fprintf o "open Nat_num\n";
                 Printf.fprintf o "open %s\n\n" m.module_name;
                 Printf.fprintf o "type 'a set = 'a Pset.set\n\n";
-  
+
                 Printf.fprintf o "%s" "let run_test n loc b =\n  if b then (Format.printf \"%s : ok\\n\" n) else (Format.printf \"%s : FAILED\\n  %s\\n\\n\" n loc);;\n\n";
 
                 Printf.fprintf o "%s" (Ulib.Text.to_string r_extra);
                 close_output_with_check ext_o
              end in ()
           end
-      | Some(Typed_ast.Target_isa) -> 
+      | Some(Typed_ast.Target_isa) ->
           begin
           try begin
             let (r_main, r_extra_opt) = B.isa_defs m.typed_ast in
             let r1 = B.isa_header_defs m.typed_ast in
-            let _ = 
+            let _ =
             begin
-                let (o, ext_o) = open_output_with_check (m.module_name ^ ".thy") in 
+                let (o, ext_o) = open_output_with_check (m.module_name ^ ".thy") in
                 Printf.fprintf o "header{*%s*}\n\n" (generated_line m.filename);
                 Printf.fprintf o "theory \"%s\" \n\n" m.module_name;
                 Printf.fprintf o "imports \n \t Main\n";
@@ -282,8 +282,8 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
                  *)
                 Printf.fprintf o "%s" (Ulib.Text.to_string r1);
 
-                begin 
-                  if m.predecessor_modules <> [] then 
+                begin
+                  if m.predecessor_modules <> [] then
                     begin
                       List.iter (fun f -> Printf.fprintf o "\t \"%s\" \n" f) m.predecessor_modules;
                     end
@@ -298,7 +298,7 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
 
               let _ = match r_extra_opt with None -> () | Some r_extra ->
               begin
-                let (o, ext_o) = open_output_with_check (m.module_name ^ "Extra.thy") in              
+                let (o, ext_o) = open_output_with_check (m.module_name ^ "Extra.thy") in
                 Printf.fprintf o "header{*%s*}\n\n" (generated_line m.filename);
                 Printf.fprintf o "theory \"%sExtra\" \n\n" m.module_name;
                 Printf.fprintf o "imports \n \t Main \"~~/src/HOL/Library/Efficient_Nat\" \"%s\"\n" m.module_name;
@@ -312,7 +312,7 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
                     raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans_header (l, msg)))
           end
 
-      | Some(Typed_ast.Target_coq) -> 
+      | Some(Typed_ast.Target_coq) ->
           begin
             let r = B.coq_defs m.typed_ast in
             let (o, ext_o) = open_output_with_check (f' ^ ".v") in
@@ -335,7 +335,7 @@ let output libpath isa_thy targ consts type_info mods alldoc_accum alldoc_inc_ac
     mods
 
 
-let output_alldoc f' fs alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum = 
+let output_alldoc f' fs alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
   let rs = !alldoc_accum in
   let (o, ext_o) = open_output_with_check (f' ^ ".tex") in
   Printf.fprintf o "%%%s\n" (generated_line fs);
diff --git a/src/process_file.mli b/src/process_file.mli
index 55dbc6d1..b7b70def 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -50,7 +50,7 @@ val parse_file : string -> Parse_ast.defs * Parse_ast.lex_skips
 
 (* type instances = Types.instance list Types.Pfmap.t
 
-val check_ast_as_module : 
+val check_ast_as_module :
   Targetset.t ->
   Name.t list ->
   (Types.type_defs * instances) * env ->
@@ -59,7 +59,7 @@ val check_ast_as_module :
   (Types.type_defs * instances * instances) * env *
   (def list * Ast.lex_skips)
 
-val check_ast : 
+val check_ast :
   Targetset.t ->
   Name.t list ->
   (Types.type_defs * instances) * env ->
@@ -67,10 +67,10 @@ val check_ast :
   (Types.type_defs * instances * instances) * env *
   (def list * Ast.lex_skips)
 
-val output : 
+val output :
   string ->                           (* The path to the library *)
   string ->                           (* Isabelle Theory to be included *)
-  target option ->                    (* Backend name (None for the identity backend) *) 
+  target option ->                    (* Backend name (None for the identity backend) *)
   Typed_ast.var_avoid_f ->
   (Types.type_defs * instances) -> (* The full environment built after all typechecking, and transforming *)
   checked_module list ->              (* The typechecked modules *)