Merge PR #841: Timorous fix of bug #5598 on global existing class in sections

1 files changed, 25 insertions, 10 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d4fa266c0..375a8a983 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -84,8 +84,8 @@ type instance = {
   is_class: global_reference;
   is_info: Vernacexpr.hint_info_expr;
   (* Sections where the instance should be redeclared,
-     -1 for discard, 0 for none. *)
-  is_global: int;
+     None for discard, Some 0 for none. *)
+  is_global: int option;
   is_poly: bool;
   is_impl: global_reference;
 }
@@ -98,9 +98,11 @@ let hint_priority is = is.is_info.Vernacexpr.hint_priority
 
 let new_instance cl info glob poly impl =
   let global =
-    if glob then Lib.sections_depth ()
-    else -1
+    if glob then Some (Lib.sections_depth ())
+    else None
   in
+  if match global with Some n -> n>0 && isVarRef impl | _ -> false then
+    CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable.");
     { is_class = cl.cl_impl;
       is_info = info ;
       is_global = global ;
@@ -350,22 +352,34 @@ let subst_instance (subst, (action, inst)) = action,
       is_impl = fst (subst_global subst inst.is_impl) }
 
 let discharge_instance (_, (action, inst)) =
-  if inst.is_global <= 0 then None
-  else Some (action,
+  match inst.is_global with
+  | None -> None
+  | Some n ->
+    assert (not (isVarRef inst.is_impl));
+    Some (action,
     { inst with 
-      is_global = pred inst.is_global;
+      is_global = Some (pred n);
       is_class = Lib.discharge_global inst.is_class;
       is_impl = Lib.discharge_global inst.is_impl })
     
 
-let is_local i = Int.equal i.is_global (-1)
+let is_local i = (i.is_global == None)
+
+let is_local_for_hint i =
+  match i.is_global with
+  | None -> true  (* i.e. either no Global keyword not in section, or in section *)
+  | Some n -> n <> 0 (* i.e. in a section, declare the hint as local
+     since discharge is managed by rebuild_instance which calls again
+     add_instance_hint; don't ask hints to take discharge into account
+     itself *)
 
 let add_instance check inst =
   let poly = Global.is_polymorphic inst.is_impl in
-  add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) 
+  let local = is_local_for_hint inst in
+  add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local
     inst.is_info poly;
   List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
-    (is_local inst) pri poly)
+    local pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
        (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
 
@@ -404,6 +418,7 @@ let declare_instance info local glob =
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
+      assert (not (isVarRef glob) || local);
       add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
     | None -> ()