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/record.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'vernac/record.ml')

diff --git a/vernac/record.ml b/vernac/record.ml
index bd5b71cd6b..79abf94726 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -557,7 +557,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
       Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
-        | Some b -> Some ((if b then Backward else Forward), List.hd priorities)
+        | Some () -> Some (Backward, List.hd priorities)
         | None -> None
       in
       [cref, [Name proj_name, sub, Some proj_cst]]
@@ -568,8 +568,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
         params template ~kind:Decls.Method ~name:[|binder_name|] record_data
       in
        let coers = List.map2 (fun coe pri ->
-                              Option.map (fun b ->
-                              if b then Backward, pri else Forward, pri) coe)
+                              Option.map (fun () -> Backward, pri) coe)
           coers priorities
        in
       let map ind =
-- 
cgit v1.2.3


From f16290030b48dedf3091334af4cd21a7df157381 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Sep 2020 13:21:02 +0200
Subject: Further simplification of the typeclass registration API.

---
 vernac/record.ml | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'vernac/record.ml')

diff --git a/vernac/record.ml b/vernac/record.ml
index 79abf94726..89acd79dda 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -557,10 +557,15 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
       Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
-        | Some () -> Some (Backward, List.hd priorities)
+        | Some () -> Some (List.hd priorities)
         | None -> None
       in
-      [cref, [Name proj_name, sub, Some proj_cst]]
+      let m = {
+        meth_name = Name proj_name;
+        meth_info = sub;
+        meth_const = Some proj_cst;
+      } in
+      [cref, [m]]
     | _ ->
       let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false,
                          List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
@@ -568,13 +573,17 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
         params template ~kind:Decls.Method ~name:[|binder_name|] record_data
       in
        let coers = List.map2 (fun coe pri ->
-                              Option.map (fun () -> Backward, pri) coe)
+                              Option.map (fun () -> pri) coe)
           coers priorities
        in
       let map ind =
-        let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
-          (List.rev fields) coers (Recordops.lookup_projections ind)
-        in GlobRef.IndRef ind, l
+        let map decl b y = {
+          meth_name = RelDecl.get_name decl;
+          meth_info = b;
+          meth_const = y;
+        } in
+        let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in
+        GlobRef.IndRef ind, l
       in
       List.map map inds
   in
-- 
cgit v1.2.3