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

4 files changed, 35 insertions, 12 deletions

diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index dd24aa3db..104977aef 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -20,7 +20,7 @@ let set_transparency cl b =
   List.iter (fun r ->
     let gr = Smartlocate.global_with_alias r in
     let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in
-      Classes.set_typeclass_transparency ev false b) cl
+      Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl
 
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
 | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
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 -> ()
 
diff --git a/test-suite/bugs/closed/5598.v b/test-suite/bugs/closed/5598.v
new file mode 100644
index 000000000..55fef1a57
--- /dev/null
+++ b/test-suite/bugs/closed/5598.v
@@ -0,0 +1,8 @@
+(* Checking when discharge of an existing class is possible *)
+Section foo.
+  Context {T} (a : T) (b : T).
+  Let k := eq_refl a.
+  Existing Class eq.
+  Fail Global Existing Instance k.
+  Existing Instance k.
+End foo.
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 28aeaa725..a4fe49020 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -650,7 +650,7 @@ let declare_obligation prg obl body ty uctx =
       let constant = Declare.declare_constant obl.obl_name ~local:true
 	(DefinitionEntry ce,IsProof Property)
       in
-	if not opaque then add_hint false prg constant;
+	if not opaque then add_hint (Locality.make_section_locality None) prg constant;
 	definition_message obl.obl_name;
 	true, { obl with obl_body =
 	    if poly then