Export definition of type implicits_list for contribs + fixed a

discharge bug of implicit arguments related to commit 13484 (multiple
implicit arguments sequences patch).

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

3 files changed, 19 insertions, 6 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 56ca3421de..993e33b329 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -366,7 +366,7 @@ let set_manual_implicits env flags enriching autoimps l =
 let compute_semi_auto_implicits env f manual t =
   match manual with
   | [] ->
-      if not f.auto then []
+      if not f.auto then [DefaultImpArgs, []]
       else let _,l = compute_implicits_flags env f false t in
 	     [DefaultImpArgs, prepare_implicits f l]
   | _ ->
@@ -453,7 +453,7 @@ type implicit_discharge_request =
 let implicits_table = ref Refmap.empty
 
 let implicits_of_global ref =
-  try Refmap.find ref !implicits_table with Not_found -> []
+  try Refmap.find ref !implicits_table with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
   implicits_table := Refmap.add ref imps !implicits_table
@@ -483,7 +483,7 @@ let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
   | DefaultImpArgs -> DefaultImpArgs
 
-let add_section_impls vars extra_impls (cond,impls)=
+let add_section_impls vars extra_impls (cond,impls) =
   let p = List.length vars - List.length extra_impls in
   adjust_side_condition p cond, extra_impls @ impls
 
@@ -660,12 +660,14 @@ let rec drop_first_implicits p l =
       drop_first_implicits (p-1) (LessArgsThan n,impls)
 
 let rec select_impargs_size n = function
-  | [] -> []
+  | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
   | [_, impls] | (DefaultImpArgs, impls)::_ -> impls
   | (LessArgsThan p, impls)::l ->
       if n <= p then impls else select_impargs_size n l
 
-let rec select_stronger_impargs = function [] -> [] | (_,impls)::_ -> impls
+let rec select_stronger_impargs = function
+  | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
+  | (_,impls)::_ -> impls
 
 (*s Registration as global tables *)
 
diff --git a/library/impargs.mli b/library/impargs.mli
index f71607ec91..a4553b0fca 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -51,7 +51,10 @@ type implicit_explanation =
   | Manual
 
 type implicit_status = (identifier * implicit_explanation * (bool * bool)) option
-type implicits_list (* = implicit_status list *)
+
+type implicit_side_condition
+
+type implicits_list = implicit_side_condition * implicit_status list
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index b142ba7723..ce3e692f4a 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -99,3 +99,11 @@ Parameter p : forall A, A -> forall n, n = 0 -> True.
 Implicit Arguments p [A n].
 Notation Q := (p 0).
 Check Q eq_refl.
+
+(* Check implicits with Context *)
+
+Section C.
+Context {A:Set}.
+Definition h (a:A) := a.
+End C.
+Check h 0.