aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.mli
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-02 22:30:29 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-02 22:30:29 +0000
commit401f17afa2e9cc3f2d734aef0d71a2c363838ebd (patch)
tree7a3e0ce211585d4c09a182aad1358dfae0fb38ef /toplevel/vernac.mli
parent15cb1aace0460e614e8af1269d874dfc296687b0 (diff)
Noise for nothing
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernac.mli')
-rw-r--r--toplevel/vernac.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index d89e90d0c..1cfd94e05 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -12,16 +12,16 @@
Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
- Util.loc * Vernacexpr.vernac_expr
+ Pp.loc * Vernacexpr.vernac_expr
(** Reads and executes vernac commands from a stream.
The boolean [just_parsing] disables interpretation of commands. *)
-exception DuringCommandInterp of Util.loc * exn
+exception DuringCommandInterp of Pp.loc * exn
exception End_of_input
val just_parsing : bool ref
-val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
+val eval_expr : Pp.loc * Vernacexpr.vernac_expr -> unit
val raw_do_vernac : Pcoq.Gram.parsable -> unit
(** Set XML hooks *)