diff options
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/library/impargs.mli b/library/impargs.mli index f43880e29..2eab1af66 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -12,8 +12,10 @@ open Term open Environ open Nametab -(** {6 Sect } *) -(** Implicit arguments. Here we store the implicit arguments. Notice that we +(** Implicit Arguments *) + +(** {6 ... } *) +(** Here we store the implicit arguments. Notice that we are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> unit @@ -33,7 +35,7 @@ val is_maximal_implicit_args : unit -> bool type implicits_flags val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b -(** {6 Sect } *) +(** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments of a reference can be automatically infered *) |