Fix implicit args code so that declarations are added for all

definitions and variables (may increase the vo's size a bit), which in
turn fixes discharging with manual implicit args only. 
Fix Context to correctly handle "kept" assumptions for typeclasses,
discharging a class variable when any variable bound in it is used.


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

5 files changed, 20 insertions, 17 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 9e242d2b31..a973e6a55e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -46,7 +46,7 @@ let add_cache_hook f = cache_hook := f
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
+  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
@@ -61,7 +61,7 @@ let cache_variable ((sp,_),o) =
     | SectionLocalAssum (ty, impl, keep) ->
         let cst = Global.push_named_assum (id,ty) in
 	let impl = if impl then Lib.Implicit else Lib.Explicit in
-	let keep = if keep then Some ty else None in
+	let keep = if keep <> [] then Some (ty, keep) else None in
 	impl, true, cst, keep
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
diff --git a/library/declare.mli b/library/declare.mli
index 38b1fa7b2e..32b6511220 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,7 +34,7 @@ open Nametab
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
+  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 725af0e9ac..b4b61461f4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -546,22 +546,19 @@ let declare_implicits local ref =
       
 let declare_var_implicits id =
   let flags = !implicit_args in
-    if flags.auto then
-      declare_implicits_gen ImplLocal flags (VarRef id)
+    declare_implicits_gen ImplLocal flags (VarRef id)
 
 let declare_constant_implicits con =
   let flags = !implicit_args in
-    if flags.auto then
-      declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
+    declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
 
 let declare_mib_implicits kn =
   let flags = !implicit_args in
-    if flags.auto then
-      let imps = array_map_to_list
-	(fun (ind,cstrs) -> ind::(Array.to_list cstrs))
-	(compute_mib_implicits flags [] kn) in
-	add_anonymous_leaf
-	  (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
+  let imps = array_map_to_list
+    (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
+    (compute_mib_implicits flags [] kn) in
+    add_anonymous_leaf
+      (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
       
 (* Declare manual implicits *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) 
diff --git a/library/lib.ml b/library/lib.ml
index dfe00fae51..356f90b227 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -452,7 +452,7 @@ type variable_context = variable_info list
 type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
@@ -460,11 +460,15 @@ let add_section () =
 let add_section_variable id impl keep =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
+    | (vars,repl,abs)::sl ->
+	sectab := ((id,impl,keep)::vars,repl,abs)::sl
 
 let rec extract_hyps = function
   | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
-  | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
+  | ((id,impl,Some (ty,keep))::idl,hyps) -> 
+      if List.exists (fun (id,_,_) -> List.mem id keep) hyps then
+	(id,impl,None,ty) :: extract_hyps (idl,hyps)
+      else extract_hyps (idl,hyps)
   | (id::idl,hyps) -> extract_hyps (idl,hyps)
   | [], _ -> []
 
diff --git a/library/lib.mli b/library/lib.mli
index dc8202ed2a..3330a20a79 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -182,7 +182,9 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont
 val section_instance : Libnames.global_reference -> Names.identifier array
 val is_in_section : Libnames.global_reference -> bool
 
-val add_section_variable : Names.identifier -> binding_kind -> Term.types option -> unit
+val add_section_variable : Names.identifier -> binding_kind -> 
+  (Term.types * Names.identifier list) option -> unit
+
 val add_section_constant : Names.constant -> Sign.named_context -> unit
 val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
 val replacement_context : unit ->