Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.typeclass

6 files changed, 11 insertions, 12 deletions

diff --git a/API/API.mli b/API/API.mli
index 24a99d57f..e46bca85f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4308,7 +4308,7 @@ sig
   type typeclass = {
     cl_univs : Univ.AUContext.t;
     cl_impl : Globnames.global_reference;
-    cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t;
+    cl_context : Globnames.global_reference option list * Context.Rel.t;
     cl_props : Context.Rel.t;
     cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option
                 * Names.Constant.t option) list;
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index f7c36c4e5..bfe73160b 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
+  Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
   Constrexpr.constr_expr * Id.Set.t
 
 val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
+  (Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
     Constrexpr.constr_expr * Id.Set.t) ->
   constr_expr -> constr_expr * Id.Set.t
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bbb3a1bb2..bc9990d02 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -65,7 +65,7 @@ type typeclass = {
   cl_impl : global_reference;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (global_reference * bool) option list * Context.Rel.t;
+  cl_context : global_reference option list * Context.Rel.t;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Context.Rel.t;
@@ -175,7 +175,7 @@ let subst_class (subst,cl) =
   and do_subst_gr gr = fst (subst_global subst gr) in
   let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in
   let do_subst_context (grs,ctx) =
-    List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
+    List.smartmap (Option.smartmap do_subst_gr) grs,
     do_subst_ctx ctx in
   let do_subst_projs projs = List.smartmap (fun (x, y, z) -> 
     (x, y, Option.smartmap do_subst_con z)) projs in
@@ -213,10 +213,10 @@ let discharge_class (_,cl) =
       let newgrs = List.map (fun decl ->
 			     match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with
 			     | None -> None
-			     | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
+                             | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
 			    ctx'
       in
-      List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+      List.smartmap (Option.smartmap Lib.discharge_global) grs
       @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 8ee061330..0cbe1c71c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -25,9 +25,8 @@ type typeclass = {
   cl_impl : global_reference;
 
   (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
-     The boolean indicates if the typeclass argument is a direct superclass and the global reference
-     gives a direct link to the class itself. *)
-  cl_context : (global_reference * bool) option list * Context.Rel.t;
+      The global reference gives a direct link to the class itself. *)
+  cl_context : global_reference option list * Context.Rel.t;
 
   (** Context of definitions and properties on defs, will not be shared *)
   cl_props : Context.Rel.t;
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c2e9a5ab4..6914f899b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -141,7 +141,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
 	  (fun avoid (clname, _) ->
 	    match clname with
-	    | Some (cl, b) ->
+            | Some cl ->
 		let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
diff --git a/vernac/record.ml b/vernac/record.ml
index 114b55cb4..a7eb19dc8 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -523,7 +523,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
   let ctx_context =
     List.map (fun decl ->
       match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with
-      | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
+      | Some (_, ((cl,_), _)) -> Some cl.cl_impl
       | None -> None)
       params, params
   in