diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-27 15:50:18 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-27 15:50:18 +0000 |
commit | 653f63e8b49fd46e686619d8e847e571d8c5442a (patch) | |
tree | 388c2ca80ddc69944f1fe708e629e925b7d7df60 /pretyping | |
parent | 1b127e845bb8043de12c965d0407a23bfb5def70 (diff) |
Fix implementation of "Global Instance" which redeclared the same
instance multiple times at each section closing (still a hack).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11338 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/typeclasses.ml | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 04b34db38..9bcf8116c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -46,14 +46,13 @@ type typeclass = { type typeclasses = (global_reference, typeclass) Gmap.t -type globality = int option - type instance = { is_class: global_reference; is_pri: int option; - is_global: globality; (* Sections where the instance should be redeclared, - Some n for n sections, None for discard at end of section. *) + -1 for discard, 0 for none, mutable to avoid redeclarations + when multiple rebuild_object happen. *) + is_global: int ref; is_impl: constant; } @@ -64,13 +63,13 @@ let instance_impl is = is.is_impl let new_instance cl pri glob impl = let global = if Lib.sections_are_opened () then - if glob then Some (Lib.sections_depth ()) - else None - else Some 0 + if glob then Lib.sections_depth () + else -1 + else 0 in { is_class = cl.cl_impl; is_pri = pri ; - is_global = global ; + is_global = ref global ; is_impl = impl } let classes : typeclasses ref = ref Gmap.empty @@ -112,7 +111,7 @@ let gmap_cmap_merge old ne = ne Gmap.empty in Gmap.fold (fun cl insts acc -> - if Gmap.mem cl ne' then acc + if Gmap.mem cl acc then acc else Gmap.add cl insts acc) old ne' @@ -220,13 +219,13 @@ let rebuild (cl,m,inst) = let inst = Gmap.map (fun insts -> Cmap.fold (fun k is insts -> - match is.is_global with - | None -> insts - | Some 0 -> Cmap.add k is insts - | Some n -> + match !(is.is_global) with + | -1 -> insts + | 0 -> Cmap.add k is insts + | n -> add_instance_hint is.is_impl is.is_pri; - let is' = { is with is_global = Some (pred n) } - in Cmap.add k is' insts) insts Cmap.empty) + is.is_global := pred n; + Cmap.add k is insts) insts Cmap.empty) inst in (cl, m, inst) |