Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 22caa2a9f..b2509d011 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -19,21 +19,21 @@ type input_buffer = {
   mutable tokens : Gram.parsable; (* stream of tokens *)
   mutable start : int } (* stream count of the first char of the buffer *)
 
-(* The input buffer of stdin *)
+(* The input buffer of stdin. *)
 
 val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
 (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
   May raise only the following exceptions: [Drop] and [End_of_input],
-  meaning we get out of the Coq loop *)
+  meaning we get out of the Coq loop. *)
 
 val print_toplevel_error : exn -> std_ppcmds
 
-(* Parse and execute a vernac command *)
+(* Parse and execute a vernac command. *)
 
 val do_vernac : unit -> unit
 
-(* Main entry point of Coq: read and execute vernac commands *)
+(* Main entry point of Coq: read and execute vernac commands. *)
 
 val loop : unit -> unit