diff options
Diffstat (limited to 'toplevel/vernac.mli')
| -rw-r--r-- | toplevel/vernac.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index c9714f8c9..0d9f5871a 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -14,13 +14,10 @@ val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -(** Reads and executes vernac commands from a stream. - The boolean [just_parsing] disables interpretation of commands. *) +(** Reads and executes vernac commands from a stream. *) exception End_of_input -val just_parsing : bool ref - val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit (** Set XML hooks *) |