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

4 files changed, 27 insertions, 7 deletions

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