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.
---
 tactics/class_tactics.ml | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b4d7e7d7f0..ed92a85a12 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -483,17 +483,7 @@ let make_resolve_hyp env sigma st only_classes pri decl =
     if keep then
       let id = GlobRef.VarRef id in
       let name = PathHints [id] in
-      let hints =
-        if is_class then
-          let hints = build_subclasses ~check:false env sigma id empty_hint_info in
-            (List.map_append
-             (fun (path,info,c) ->
-              let h = IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in
-              make_resolves env sigma ~name:(PathHints path) info ~check:true h)
-               hints)
-        else []
-      in
-        (hints @ make_resolves env sigma pri ~name ~check:false (IsGlobRef id))
+        (make_resolves env sigma pri ~name ~check:false (IsGlobRef id))
     else []
 
 let make_hints g (modes,st) only_classes sign =
-- 
cgit v1.2.3