[toplevel] Remove unused parameter from `Vernac.process_expr`.

3 files changed, 12 insertions, 8 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b608488c8..9a4f476bd 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -300,7 +300,7 @@ let do_vernac sid =
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
-    Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input))
+    Vernac.process_expr sid (read_sentence sid (fst input))
   with
     | Stm.End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
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 ()
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index e75f8f9e8..bbc095c68 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -8,11 +8,15 @@
 
 (** Parsing of vernacular. *)
 
-(** Reads and executes vernac commands from a stream. *)
-val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
+(** [process_expr sid cmd] Executes vernac command [cmd]. Callers are
+    expected to handle and print errors in form of exceptions, however
+    care is taken so the state machine is left in a consistent
+    state. *)
+val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
 
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
-    echo the commands if [echo] is set. *)
+    echo the commands if [echo] is set. Callers are expected to handle
+    and print errors in form of exceptions. *)
 val load_vernac : bool -> Stateid.t -> string -> Stateid.t
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)