Pb quand une meme classe est definie dans 2 fichiers

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

1 files changed, 9 insertions, 3 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 3bc1292ea..c7df3229d 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -63,12 +63,13 @@ module Bijint = struct
   let map x b = if 0 <= x & x < b.s then b.v.(x) else raise Not_found
   let revmap y b = let n = Gmap.find y b.inv in (n, snd (b.v.(n)))
   let add x y b =
-    if mem x b then failwith "Bijint.add";
     let v =
       if b.s = Array.length b.v then
 	(let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v)
       else b.v in
     v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = Gmap.add x b.s b.inv }
+  let replace n x y b =
+    let v = Array.copy b.v in v.(n) <- (x,y); { b with v = v }
   let dom b = Gmap.dom b.inv
 end
 
@@ -90,8 +91,13 @@ let unfreeze (fcl,fco,fig) =
 
 (* ajout de nouveaux "objets" *)
 
-let add_new_class cl s = 
-  class_tab := Bijint.add cl s !class_tab
+let add_new_class cl s =
+  try
+    let n,s' = Bijint.revmap cl !class_tab in
+    if s.cl_strength = Global & s'.cl_strength <> Global then
+      class_tab := Bijint.replace n cl s !class_tab
+  with Not_found ->
+    class_tab := Bijint.add cl s !class_tab
 
 let add_new_coercion coe s = 
   coercion_tab := Gmap.add coe s !coercion_tab