Dead code in impargs (afaics, no more need, since r11242, to merge

automatic and manual implicit arguments twice).

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

2 files changed, 13 insertions, 23 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 84097c840d..19f7e094ef 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -409,23 +409,16 @@ let compute_global_implicits flags manual = function
 (* Merge a manual explicitation with an implicit_status list *)
 
 let merge_impls oldimpls newimpls =
-  let (before, news), olds =
-    let len = List.length newimpls - List.length oldimpls in
-      if len >= 0 then list_chop len newimpls, oldimpls
-      else
-	let before, after = list_chop (-len) oldimpls in
-	  (before, newimpls), after
-  in
-    before @ (List.map2 (fun orig ni ->
-      match orig with
-      | Some (_, Manual, _) -> orig
-      | _ -> ni) olds news)
+  List.map2 (fun orig ni ->
+    match orig with
+    | Some (_, Manual, _) -> orig
+    | _ -> ni) oldimpls newimpls
 
 (* Caching implicits *)
 
 type implicit_interactive_request =
   | ImplAuto
-  | ImplManual of implicit_status list
+  | ImplManual
 
 type implicit_discharge_request =
   | ImplLocal
@@ -507,16 +500,13 @@ let rebuild_implicits (req,l) =
 	  let oldimpls = snd (List.hd l) in
 	  let newimpls = compute_global_implicits flags [] ref in
 	    [ref,merge_impls oldimpls newimpls]
-      | ImplManual m ->
+      | ImplManual ->
 	  let oldimpls = snd (List.hd l) in
-	  let auto =
-	    if flags.auto then
-	      let newimpls = compute_global_implicits flags [] ref in
-		merge_impls oldimpls newimpls
-	    else oldimpls
-	  in
-	  let l' = merge_impls auto m in
-	  [ref,l']
+	  if flags.auto then
+	    let newimpls = compute_global_implicits flags [] ref in
+	    [ref, merge_impls oldimpls newimpls]
+	  else
+	    [ref,oldimpls]
 
 let classify_implicits (req,_ as obj) =
   if req = ImplLocal then Dispose else Substitute obj
@@ -572,7 +562,7 @@ let declare_manual_implicits local ref ?enriching l =
   let l' = compute_manual_implicits env flags t enriching l in
   let req =
     if is_local local ref then ImplLocal
-    else ImplInteractive(ref,flags,ImplManual l')
+    else ImplInteractive(ref,flags,ImplManual)
   in
     add_anonymous_leaf (inImplicits (req,[ref,l']))
 
diff --git a/library/impargs.mli b/library/impargs.mli
index 90ffb68590..84f3275638 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -103,7 +103,7 @@ val merge_impls : implicits_list -> implicits_list -> implicits_list
 
 type implicit_interactive_request =
   | ImplAuto
-  | ImplManual of implicit_status list
+  | ImplManual
 
 type implicit_discharge_request =
   | ImplLocal