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
---
 pretyping/typeclasses.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index da30b20578..d54eaf00ee 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -197,8 +197,8 @@ let discharge (_,(cl,m,inst)) =
 	let ctx = abs_context cl in
 	{ cl with cl_impl = cl_impl';
 	  cl_context = 
-	    List.map (fun (na,b,t) -> None, (Name na,b,t)) ctx @
-	      (discharge_context (List.map pi1 ctx) cl.cl_context);
+	    List.map (fun (na,impl,b,t) -> None, (Name na,b,t)) ctx @
+	      (discharge_context (List.map (fun (na, _, _, _) -> na) ctx) cl.cl_context);
 	  cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs }
     in Gmap.add cl_impl' cl' acc
   in
@@ -216,7 +216,7 @@ let discharge (_,(cl,m,inst)) =
   let instances = Gmap.fold subst_inst inst Gmap.empty in
     Some (classes, m, instances)
       
-let rebuild (_,(cl,m,inst)) =
+let rebuild (cl,m,inst) =
   let inst = 
     Gmap.map (fun insts -> 
       Cmap.fold (fun k is insts -> 
-- 
cgit v1.2.3