From 2debc4ab0b171963afff40cc3183e4e92cca9a0e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 22 Jul 2008 14:02:22 +0000
Subject: 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
---
 toplevel/classes.ml       | 14 ++++++++------
 toplevel/vernacentries.ml |  8 ++++++++
 2 files changed, 16 insertions(+), 6 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e4df5acbfa..9f3b3343cb 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)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 65b36edb60..afa667ad91 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -782,6 +782,14 @@ let _ =
       optread  = Impargs.is_implicit_args;
       optwrite = Impargs.make_implicit_args }
 
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "manual implicit arguments";
+      optkey   = (TertiaryTable ("Manual","Implicit","Arguments"));
+      optread  = Impargs.is_manual_implicit_args;
+      optwrite = Impargs.make_manual_implicit_args }
+
 let _ =
   declare_bool_option 
     { optsync  = true;
-- 
cgit v1.2.3