From ed5d9cb136384ce0f7363a1c839ff0f9a7e9df7b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 26 Jun 2009 17:16:23 +0000
Subject: Add doc for [Print Opaque Dependencies] and a better explanation for
 the flags of manual implicit arguments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12211 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/impargs.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/impargs.mli b/library/impargs.mli
index 90b6052231..9f67eb4624 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -66,7 +66,8 @@ val positions_of_implicits : implicits_list -> int list
 val compute_implicits : env -> types -> implicits_list
 
 (* A [manual_explicitation] is a tuple of a positional or named explicitation with
-   maximal insertion, force inference and force usage flags. *)
+   maximal insertion, force inference and force usage flags. Forcing usage makes 
+   the argument implicit even if the automatic inference considers it not inferable. *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
 val compute_implicits_with_manual : env -> types -> bool -> 
-- 
cgit v1.2.3