From e3a1cf35313bbc4eaca2a43f5fc95ca306bc45fa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Sep 2020 11:14:23 +0200
Subject: Remove the forward class hint feature.

It was not documented, not properly tested and thus likely buggy. Judging
from the code alone I spotted already one potential bug. Further more it was
prominently making use of the infamous "arbitrary term as hint" feature.

Since the only user in our CI seems to be a math-classes file that introduced
the feature under a claim of "cleanup", I believe we can safely remove it
without anyone noticing.
---
 vernac/classes.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index b38a249b73..3485d17951 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -58,13 +58,7 @@ let is_local_for_hint i =
 let add_instance_base inst =
   let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in
   add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality
-    inst.is_info;
-  List.iter (fun (path, pri, c) ->
-    let h = Hints.IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in
-    add_instance_hint h path
-                ~locality pri)
-    (build_subclasses ~check:(not (isVarRef inst.is_impl))
-       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
+    inst.is_info
 
 let mk_instance cl info glob impl =
   let global =
-- 
cgit v1.2.3