aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.mli
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-09-28 15:23:14 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-09-28 15:23:14 +0000
commitea5408dc21bd8748e7d9917e8deaf9c639883475 (patch)
tree751361fa626263d984a70501d5e4206cb03b1554 /toplevel/vernac.mli
parent5b95fb206ab93a94736d8e5343326ff44953189e (diff)
corrections pour ocamlweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@88 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 401598781..0c65b8693 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -3,18 +3,18 @@
(* Parsing of vernacular. *)
-(* Like Exc_located, but specifies the outermost file read, the input buffer
+(* Like [Exc_located], but specifies the outermost file read, the input buffer
associated to the location of the error, and the error itself. *)
exception Error_in_file of string * (string * Coqast.loc) * exn
(* Read a vernac command on the specified input (parse only).
- Raises End_of_file if EOF (or Ctrl-D) is reached. *)
+ Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
val parse_phrase : Pcoq.Gram.parsable * in_channel option -> Coqast.t
(* Reads and executes vernac commands from a stream.
- The boolean just_parsing disables interpretation of commands. *)
+ The boolean [just_parsing] disables interpretation of commands. *)
exception DuringCommandInterp of Coqast.loc * exn
exception End_of_input