Remove unused is_class info from cl_context

5 files changed, 22 insertions, 41 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 0f05cc5e10..2853eef5c5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -199,8 +199,7 @@ let implicit_application env ty =
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let c = class_info env sigma gr in
-    let (ci, rd) = c.cl_context in
-    let args, avoid = combine_params avoid par (List.rev rd) in
+    let args, avoid = combine_params avoid par (List.rev c.cl_context) in
     CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
 
 let warn_ignoring_implicit_status =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7479a63762..51b228a640 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -56,7 +56,7 @@ type typeclass = {
   cl_impl : GlobRef.t;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : bool list * Constr.rel_context;
+  cl_context : Constr.rel_context;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Constr.rel_context;
@@ -97,7 +97,7 @@ let instances : instances ref = Summary.ref GlobRef.Map.empty ~name:"instances"
 let typeclass_univ_instance (cl, u) =
   assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
   let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in
-    { cl with cl_context = on_snd subst_ctx cl.cl_context;
+    { cl with cl_context = subst_ctx cl.cl_context;
       cl_props = subst_ctx cl.cl_props}
 
 let class_info env sigma c =
@@ -178,7 +178,7 @@ let remove_instance inst =
 
 
 let instance_constructor (cl,u) args =
-  let lenpars = List.count is_local_assum (snd cl.cl_context) in
+  let lenpars = List.count is_local_assum cl.cl_context in
   let open EConstr in
   let pars = fst (List.chop lenpars args) in
     match cl.cl_impl with
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ea67ca273e..b749b978c3 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -36,9 +36,9 @@ type typeclass = {
   (** The class implementation: a record parameterized by the context with defs in it or a definition if
      the class is a singleton. This acts as the class' global identifier. *)
 
-  cl_context : bool list * Constr.rel_context;
-  (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
-      The bool says whether we are at a class. *)
+  cl_context : Constr.rel_context;
+  (** Context in which the definitions are typed.
+      Includes both typeclass parameters and superclasses. *)
 
   cl_props : Constr.rel_context;
   (** Context of definitions and properties on defs, will not be shared *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 31d04c1b0d..d5509e2697 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -165,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 = on_snd do_subst_ctx 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;
@@ -194,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 -> false
-          | Some _ -> true)
-          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;
@@ -321,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
@@ -396,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
@@ -527,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 54fd1b2c51..968d8aed30 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -587,26 +587,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 _ -> true
-      | None -> false)
-      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 =
@@ -614,7 +605,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
@@ -634,7 +625,7 @@ let add_constant_class env sigma cst =
   let tc =
     { cl_univs = univs;
       cl_impl = GlobRef.ConstRef cst;
-      cl_context = (List.map (const false) ctx, ctx);
+      cl_context = ctx;
       cl_props = [LocalAssum (make_annot Anonymous r, t)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
@@ -656,7 +647,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 false) ctx, ctx;
+        cl_context = ctx;
         cl_props = [LocalAssum (make_annot Anonymous r, ty)];
         cl_projs = [];
         cl_strict = !typeclasses_strict;