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

10 files changed, 48 insertions, 25 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 9e242d2b3..a973e6a55 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 38b1fa7b2..32b651122 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 725af0e9a..b4b61461f 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 dfe00fae5..356f90b22 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 dc8202ed2..3330a20a7 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 ->
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 389e0e722..ed8ecfac4 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -99,7 +99,7 @@ let declare_assumption env isevars idl is_coe k bl c nl =
       Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None 
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl
+      List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2d5cd659f..2df66180c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -257,6 +257,14 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
+let push_named_context = List.fold_right push_named
+
+let rec list_filter_map f = function
+  | [] -> []
+  | hd :: tl -> match f hd with
+    | None -> list_filter_map f tl
+    | Some x -> x :: list_filter_map f tl
+
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let evars = ref Evd.empty in
@@ -267,6 +275,14 @@ let context ?(hook=fun _ -> ()) l =
   let ctx = try named_of_rel_context fullctx with _ -> 
     error "Anonymous variables not allowed in contexts."
   in
+  let env = push_named_context ctx env in
+  let keeps = 
+    List.fold_left (fun acc (id,_,t) ->
+      match class_of_constr t with
+      | None -> acc
+      | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc)
+      [] ctx
+  in
     List.iter (function (id,_,t) -> 
       if Lib.is_modtype () then 
 	let cst = Declare.declare_internal_constant id
@@ -278,10 +294,14 @@ let context ?(hook=fun _ -> ()) l =
 		hook (ConstRef cst)
 	    | None -> ()
       else (
-	let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+	let impl = List.exists (fun (x,_) -> 
+	  match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls 
+	and keep = 
+	  let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in
+	    List.concat l
 	in
 	  Command.declare_one_assumption false (Local (* global *), Definitional) t
-	    [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
+	    [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id);
 	  match class_of_constr t with
 	  | None -> ()
 	  | Some tc -> hook (VarRef id)))
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 820e0f156..d2eed98e4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1102,9 +1102,9 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
   | None ->
       (match local with
       | Local ->
-          let impl=false and keep=false in (* copy values from Vernacentries *)
+          let impl=false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum (t_i,impl,keep) in
+          let c = SectionLocalAssum (t_i,impl,[]) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
           (Local,VarRef id,imps)
       | Global ->
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 73d8516f0..d5283a6db 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -45,13 +45,13 @@ val syntax_definition : identifier -> identifier list * constr_expr ->
 
 val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
   Impargs.manual_explicitation list ->
-  bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
+  bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
   
 val set_declare_assumption_hook : (types -> unit) -> unit
 
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> 
-  bool -> bool -> bool -> unit
+  bool -> identifier list -> bool -> unit
 
 val open_temp_scopes : Topconstr.scope_name option -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 90e211d03..5d76f4ff2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -373,7 +373,7 @@ let vernac_assumption kind l nl=
 	List.iter (fun lid -> 
 	  if global then Dumpglob.dump_definition lid false "ax" 
 	  else Dumpglob.dump_definition lid true "var") idl;
-      declare_assumption idl is_coe kind [] c false false nl) l
+      declare_assumption idl is_coe kind [] c false [] nl) l
 	  
 let vernac_record k finite infer struc binders sort nameopt cfs =
   let const = match nameopt with