diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 7 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 2 |
2 files changed, 5 insertions, 4 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 8fdaedbaf..24d414c88 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -111,13 +111,14 @@ let pr_open_cur_subgoals () = (* | _ -> false *) let rec interp_vernac ~check ~interactive doc sid (loc,com) = - let interp = function + let interp v = + match under_control v with | VernacLoad (verbosely, fname) -> - let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in + let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in load_vernac ~verbosely ~check ~interactive doc sid f - | v -> + | _ -> (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index f9a430026..8a798a98e 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -12,7 +12,7 @@ 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 : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stm.doc * Stateid.t +val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle |