Merge PR #13118: [type classes] Simplify cl_context

Reviewed-by: ppedrot

2 files changed, 15 insertions, 36 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index a464eab127..d5509e2697 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -152,9 +152,6 @@ let subst_class (subst,cl) =
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr) in
   let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
-  let do_subst_context (grs,ctx) =
-    List.Smart.map (Option.Smart.map do_subst_gr) grs,
-    do_subst_ctx ctx in
   let do_subst_meth m =
     let c = Option.Smart.map do_subst_con m.meth_const in
     if c == m.meth_const then m
@@ -168,7 +165,7 @@ let subst_class (subst,cl) =
   let do_subst_projs projs = List.Smart.map do_subst_meth projs in
   { cl_univs = cl.cl_univs;
     cl_impl = do_subst_gr cl.cl_impl;
-    cl_context = do_subst_context cl.cl_context;
+    cl_context = do_subst_ctx cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
     cl_projs = do_subst_projs cl.cl_projs;
     cl_strict = cl.cl_strict;
@@ -197,25 +194,16 @@ let discharge_class (_,cl) =
       | VarRef _ | ConstructRef _ -> assert false
       | ConstRef cst -> Lib.section_segment_of_constant cst
       | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
-  let discharge_context ctx' subst (grs, ctx) =
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let grs' =
-      let newgrs = List.map (fun decl ->
-                             match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr env sigma with
-                             | None -> None
-                             | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
-                            ctx'
-      in
-      grs @ newgrs
-    in grs', discharge_rel_context subst 1 ctx @ ctx' in
+  let discharge_context ctx' subst ctx =
+    discharge_rel_context subst 1 ctx @ ctx'
+  in
   try
     let info = abs_context cl in
     let ctx = info.Section.abstr_ctx in
     let ctx, subst = rel_of_variable_context ctx in
     let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
-    let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
+    let props = discharge_rel_context (subst, usubst) (succ (List.length cl.cl_context)) cl.cl_props in
     let discharge_proj x = x in
     { cl_univs = cl_univs';
       cl_impl = cl.cl_impl;
@@ -324,7 +312,7 @@ let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma t
 let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
   let subst = List.fold_left2
       (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
-      [] subst (snd k.cl_context)
+      [] subst k.cl_context
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
@@ -399,7 +387,7 @@ let do_instance_subst_constructor_and_ty subst k u ctx =
   let subst =
     List.fold_left2 (fun subst' s decl ->
       if is_local_assum decl then s :: subst' else subst')
-    [] subst (k.cl_props @ snd k.cl_context)
+    [] subst (k.cl_props @ k.cl_context)
   in
   let (app, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr ctx in
@@ -530,7 +518,7 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   let u_s = EInstance.kind sigma u in
   let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
   let args = List.map of_constr args in
-  let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
+  let cl_context = List.map (Termops.map_rel_decl of_constr) cl.cl_context in
   let _, args =
     List.fold_right (fun decl (args, args') ->
         match decl with
diff --git a/vernac/record.ml b/vernac/record.ml
index a4bf9893d9..acc97f61c1 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -582,26 +582,17 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
       in
       List.map map inds
   in
-  let ctx_context =
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    List.map (fun decl ->
-      match Typeclasses.class_of_constr env sigma (EConstr.of_constr (RelDecl.get_type decl)) with
-      | Some (_, ((cl,_), _)) -> Some cl.cl_impl
-      | None -> None)
-      params, params
-  in
-  let univs, ctx_context, fields =
+  let univs, params, fields =
     match univs with
     | Polymorphic_entry (nas, univs) ->
       let usubst, auctx = Univ.abstract_universes nas univs in
       let usubst = Univ.make_instance_subst usubst in
       let map c = Vars.subst_univs_level_constr usubst c in
       let fields = Context.Rel.map map fields in
-      let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
-      auctx, ctx_context, fields
+      let params = Context.Rel.map map params in
+      auctx, params, fields
     | Monomorphic_entry _ ->
-      Univ.AUContext.empty, ctx_context, fields
+      Univ.AUContext.empty, params, fields
   in
   let map (impl, projs) =
     let k =
@@ -609,7 +600,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
         cl_impl = impl;
         cl_strict = !typeclasses_strict;
         cl_unique = !typeclasses_unique;
-        cl_context = ctx_context;
+        cl_context = params;
         cl_props = fields;
         cl_projs = projs }
     in
@@ -629,7 +620,7 @@ let add_constant_class env sigma cst =
   let tc =
     { cl_univs = univs;
       cl_impl = GlobRef.ConstRef cst;
-      cl_context = (List.map (const None) ctx, ctx);
+      cl_context = ctx;
       cl_props = [LocalAssum (make_annot Anonymous r, t)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
@@ -651,7 +642,7 @@ let add_inductive_class env sigma ind =
     let r = Inductive.relevance_of_inductive env ind in
       { cl_univs = univs;
         cl_impl = GlobRef.IndRef ind;
-        cl_context = List.map (const None) ctx, ctx;
+        cl_context = ctx;
         cl_props = [LocalAssum (make_annot Anonymous r, ty)];
         cl_projs = [];
         cl_strict = !typeclasses_strict;