From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/goptions.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'library/goptions.mli') diff --git a/library/goptions.mli b/library/goptions.mli index eba44a896..511986a57 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -16,11 +16,11 @@ [declare_int_option], [declare_bool_option], ... functions. Each table/option is uniquely identified by a key of type [option_name] - which consists in a list of strings. Note that for parsing constraints, + which consists in a list of strings. Note that for parsing constraints, table names must not be made of more than 2 strings while option names can be of arbitrary length. - The declaration of a table, say of name [["Toto";"Titi"]] + The declaration of a table, say of name [["Toto";"Titi"]] automatically makes available the following vernacular commands: Add Toto Titi foo. @@ -116,18 +116,18 @@ module MakeRefTable : (*s Options. *) (* These types and function are for declaring a new option of name [key] - and access functions [read] and [write]; the parameter [name] is the option name + and access functions [read] and [write]; the parameter [name] is the option name used when printing the option value (command "Print Toto Titi." *) type 'a option_sig = { - optsync : bool; + optsync : bool; optname : string; optkey : option_name; optread : unit -> 'a; optwrite : 'a -> unit } -(* When an option is declared synchronous ([optsync] is [true]), the output is +(* When an option is declared synchronous ([optsync] is [true]), the output is a synchronous write function. Otherwise it is [optwrite] *) type 'a write_function = 'a -> unit -- cgit v1.2.3