Bug discharge d'une déclaration de coercion pour une constante non définie dans la section courante

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

1 files changed, 27 insertions, 17 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6b0ed89ab4..57afbb5e55 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -446,21 +446,27 @@ let count_extra_abstractions hyps ids_to_discard =
 let defined_in_sec sp sec_sp = dirpath sp = sec_sp
 
 (* This moves the global path one step below *)
-let process_global = function
+let process_global sec_sp = function
   | VarRef _ ->
       anomaly "process_global only processes global surviving the section"
-  | ConstRef sp ->
-      let ((_,spid,spk)) = repr_path sp in
-      let newsp = Lib.make_path spid CCI in
-      ConstRef newsp
-  | IndRef (sp,i) -> 
-      let ((_,spid,spk)) = repr_path sp in
-      let newsp = Lib.make_path spid CCI in
-      IndRef (newsp,i)
-  | ConstructRef ((sp,i),j) -> 
-      let ((_,spid,spk)) = repr_path sp in
-      let newsp = Lib.make_path spid CCI in
-      ConstructRef ((newsp,i),j)
+  | ConstRef sp as x ->
+      if defined_in_sec sp sec_sp then
+        let ((_,spid,spk)) = repr_path sp in
+        let newsp = Lib.make_path spid CCI in
+        ConstRef newsp
+      else x
+  | IndRef (sp,i) as x -> 
+      if defined_in_sec sp sec_sp then
+        let ((_,spid,spk)) = repr_path sp in
+        let newsp = Lib.make_path spid CCI in
+        IndRef (newsp,i)
+      else x
+  | ConstructRef ((sp,i),j) as x -> 
+      if defined_in_sec sp sec_sp then
+        let ((_,spid,spk)) = repr_path sp in
+        let newsp = Lib.make_path spid CCI in
+        ConstructRef ((newsp,i),j)
+      else x
 
 let process_class sec_sp ids_to_discard x =
   let (cl,{cl_strength=stre; cl_param=p}) = x in
@@ -517,7 +523,11 @@ let process_cl sec_sp cl =
     | _ -> cl
 
 let process_coercion sec_sp ids_to_discard ((coe,coeinfo),cls,clt) =
-  let hyps = context_of_global_reference coe in let nargs =
-  count_extra_abstractions hyps ids_to_discard in (process_global coe,
-  coercion_strength coeinfo, coercion_identity coeinfo, process_cl
-  sec_sp cls, process_cl sec_sp clt, nargs + coercion_params coeinfo)
+  let hyps = context_of_global_reference coe in
+  let nargs = count_extra_abstractions hyps ids_to_discard in
+  (process_global sec_sp coe,
+   coercion_strength coeinfo,
+   coercion_identity coeinfo,
+   process_cl sec_sp cls,
+   process_cl sec_sp clt,
+   nargs + coercion_params coeinfo)