Correct implementation of discharging of implicit arguments and add new

setting "Set Manual Implicit Arguments" for manual-only implicits.
Fix test-suite script. This removes the discharge_info argument of
"dynamic" object's rebuild function.


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

1 files changed, 8 insertions, 6 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e4df5acbf..9f3b3343c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -492,10 +492,12 @@ let context ?(hook=fun _ -> ()) l =
 		add_instance (Typeclasses.new_instance tc None false cst);
 		hook (ConstRef cst)
 	    | None -> ()
-      else
-	(Command.declare_one_assumption false (Local (* global *), Definitional) t
-	    [] true (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
-	 match class_of_constr t with
-	     None -> ()
-	   | Some tc -> hook (VarRef id)))
+      else (
+	let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+	in
+	  Command.declare_one_assumption false (Local (* global *), Definitional) t
+	    [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
+	  match class_of_constr t with
+	  | None -> ()
+	  | Some tc -> hook (VarRef id)))
       (List.rev ctx)