Do a second pass on the treatment of user-given implicit arguments. Now

works in inductive type definitions and fixpoints. The semantics of
an implicit inductive parameter is maybe a bit weird: it is implicit in the
inductive definition of constructors and the contructor types but not in
the inductive type itself (ie. to model the fact that one rarely wants A
in vector A n to be implicit but in vnil yes). Example in test-suite/
Also, correct the handling of the implicit arguments across sections. 
Every definition which had no explicitely given implicit arguments was
treated as if we asked to do global automatic implicit arguments on
section closing. Hence some arguments were given implicit status for no
apparent reason.
Also correct and test the parsing rule which disambiguates between {wf
..} and {A ..}.


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

2 files changed, 16 insertions, 3 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 081bb58c10..9ffd103deb 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -471,9 +471,10 @@ let rebuild_implicits (req,l) =
       | ImplAuto -> [ref,compute_global_implicits flags ref]
       | ImplManual l -> 
 	  let auto = compute_global_implicits flags ref in
+	  let auto = if flags.main then auto else List.map (fun _ -> None) auto in
 	  let l' = merge_impls auto l in [ref,l']
   in (req,l')
-
+    
 
 let (inImplicits, _) =
   declare_object {(default_object "IMPLICITS") with 
@@ -530,6 +531,10 @@ let declare_manual_implicits local ref enriching l =
   in
     add_anonymous_leaf (inImplicits (req,[ref,l']))
 
+let maybe_declare_manual_implicits local ref enriching l =
+  if l = [] then ()
+  else declare_manual_implicits local ref enriching l
+
 (*s Registration as global tables *)
 
 let init () = implicits_table := Refmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index a9e6ccb91f..e7b05f4223 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -57,7 +57,7 @@ val compute_implicits : env -> types -> implicits_list
 
 (* A [manual_explicitation] is a tuple of a positional or named explicitation with
    maximal insertion and forcing flags. *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool) 
+type manual_explicitation = Topconstr.explicitation * (bool * bool)
 
 val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list
 
@@ -69,8 +69,16 @@ val declare_mib_implicits : mutual_inductive -> unit
 
 val declare_implicits : bool -> global_reference -> unit
 
-(* Manual declaration of which arguments are expected implicit *)
+(* [declare_manual_implicits local ref enriching l]
+   Manual declaration of which arguments are expected implicit.
+   Unsets implicits if [l] is empty. *)
+
 val declare_manual_implicits : bool -> global_reference -> bool ->
   manual_explicitation list -> unit
 
+(* If the list is empty, do nothing, otherwise declare the implicits. *)
+
+val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
+  manual_explicitation list -> unit
+
 val implicits_of_global : global_reference -> implicits_list