First list in cl_context is just booleans

Used only by implicit_quantifiers

5 files changed, 15 insertions, 18 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4016a3600e..c5324702dc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -150,12 +150,12 @@ let combine_params avoid applied needed =
       | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named ->
           aux (Id.List.assoc id named :: ids) avoid app need
 
-      | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need ->
+      | (x, None) :: app, (false, (LocalAssum ({binder_name=Name id}, _))) :: need ->
           aux (x :: ids) avoid app need
 
-      | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
+      | x :: app, (false, _) :: need -> aux (fst x :: ids) avoid app need
 
-      | _, (Some _, decl) :: need | [], (None, decl) :: need ->
+      | _, (true, decl) :: need | [], (false, decl) :: need ->
         let id' = next_name_away_from (RelDecl.get_name decl) avoid in
         let t' = CAst.make @@ CRef (qualid_of_ident id',None) in
         aux (t' :: ids) (Id.Set.add id' avoid) app need
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index fc71254a46..7479a63762 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 : GlobRef.t option list * Constr.rel_context;
+  cl_context : bool list * Constr.rel_context;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Constr.rel_context;
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 3f84d08a7e..ea67ca273e 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 : GlobRef.t option list * Constr.rel_context;
+  cl_context : bool list * Constr.rel_context;
   (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
-      The global reference gives a direct link to the class itself. *)
+      The bool says whether we are at a class. *)
 
   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 a464eab127..31d04c1b0d 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 = on_snd 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;
@@ -202,10 +199,10 @@ let discharge_class (_,cl) =
     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'
+          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
diff --git a/vernac/record.ml b/vernac/record.ml
index 89acd79dda..54fd1b2c51 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -592,8 +592,8 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
     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)
+      | Some _ -> true
+      | None -> false)
       params, params
   in
   let univs, ctx_context, fields =
@@ -634,7 +634,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 = (List.map (const false) ctx, ctx);
       cl_props = [LocalAssum (make_annot Anonymous r, t)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
@@ -656,7 +656,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 = List.map (const false) ctx, ctx;
         cl_props = [LocalAssum (make_annot Anonymous r, ty)];
         cl_projs = [];
         cl_strict = !typeclasses_strict;