diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-22 14:02:22 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-22 14:02:22 +0000 |
| commit | 2debc4ab0b171963afff40cc3183e4e92cca9a0e (patch) | |
| tree | 5731b43d962a6cb731ca2b3295a863be083bd7be /pretyping | |
| parent | b8c9be5ae052c936d069630a7480fd3691c1aad0 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index da30b2057..d54eaf00e 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 -> |