diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 18:36:09 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 18:43:03 +0200 |
commit | e699313c7a3829016c853b2a1541c2e9151d709c (patch) | |
tree | 107f752561421e85cd91e23977f3185e2dea1426 /toplevel/vernac.ml | |
parent | 4abb41d008fc754f21916dcac9cce49f2d04dd6d (diff) |
[toplevel] Remove unused parameter from `Vernac.process_expr`.
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r-- | toplevel/vernac.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 8bcf2114b..9ff320ee8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -117,7 +117,7 @@ let vernac_error msg = (* Stm.End_of_input -> true *) (* | _ -> false *) -let rec interp_vernac sid po (loc,com) = +let rec interp_vernac sid (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in @@ -195,7 +195,7 @@ and load_vernac verbosely sid file = Option.iter (vernac_echo loc) in_echo; checknav_simple (loc, ast); - let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in + let nsid = Flags.silently (interp_vernac !rsid) (loc, ast) in rsid := nsid done; !rsid @@ -221,9 +221,9 @@ and load_vernac verbosely sid file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr sid po loc_ast = +let process_expr sid loc_ast = checknav_deep loc_ast; - interp_vernac sid po loc_ast + interp_vernac sid loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () |