Rename files with Class in their name to make their role clearer.

We restrict to those that are actually related to typeclasses, and
perform the following renamings:

Classops --> Coercionops
Class --> ComCoercion

23 files changed, 47 insertions, 38 deletions

diff --git a/dev/base_include b/dev/base_include
index 4841db8953..96a867475d 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -60,11 +60,11 @@ open Cases
 open Pattern
 open Patternops
 open Cbv
-open Classops
+open Coercionops
 open Arguments_renaming
 open Pretyping
 open Cbv
-open Classops
+open Coercionops
 open Clenv
 open Clenvtac
 open Constr_matching
@@ -134,7 +134,7 @@ open Tacticals
 open Tactics
 open Eqschemes
 
-open Class
+open ComCoercion
 open ComDefinition
 open Indschemes
 open Ind_tables
diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
new file mode 100644
index 0000000000..a95170a455
--- /dev/null
+++ b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then
+
+    elpi_CI_REF=rename-class-files
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    mtac2_CI_REF=rename-class-files
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f7f2bcdcff..835c20a4f7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -47,7 +47,7 @@ let ppmind kn = pp(MutInd.debug_print kn)
 let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
 let ppsp sp = pp(pr_path sp)
 let ppqualid qid = pp(pr_qualid qid)
-let ppclindex cl = pp(Classops.pr_cl_index cl)
+let ppclindex cl = pp(Coercionops.pr_cl_index cl)
 let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
 
 let prrecarg = function
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 5a2144f996..133326523b 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -29,7 +29,7 @@ val ppind : Names.inductive -> unit
 val ppsp : Libnames.full_path -> unit
 val ppqualid : Libnames.qualid -> unit
 
-val ppclindex : Classops.cl_index -> unit
+val ppclindex : Coercionops.cl_index -> unit
 
 val ppscheme : 'a Ind_tables.scheme_kind -> unit
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 28f4f5aed6..cc0c1e4602 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -678,7 +678,7 @@ let remove_one_coercion inctx c =
   try match match_coercion_app c with
   | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
       let nargs = List.length args in
-      (match Classops.hide_coercion r with
+      (match Coercionops.hide_coercion r with
           | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
               (* We skip the coercion *)
               let l = List.skipn (n - pars) args in
diff --git a/interp/notation.ml b/interp/notation.ml
index 5dc1658824..93969f3718 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1430,7 +1430,7 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 (**********************************************************************)
 (* Mapping classes to scopes *)
 
-open Classops
+open Coercionops
 
 type scope_class = cl_typ
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 864e500d56..ea5125f7ec 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -271,7 +271,7 @@ val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
 (** Get the current scope bound to Sortclass, if it exists *)
 val current_type_scope_name : unit -> scope_name option
 
-val scope_class_of_class : Classops.cl_typ -> scope_class
+val scope_class_of_class : Coercionops.cl_typ -> scope_class
 
 (** Building notation key *)
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 2f26226f4e..4e7482d4af 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,11 +18,11 @@ open Tacticals.New
 
 let update_flags ()=
   let open TransparentState in
-  let f accu coe = match coe.Classops.coe_value with
+  let f accu coe = match coe.Coercionops.coe_value with
     | Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
     | _ -> accu
   in
-  let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
+  let flags = List.fold_left f TransparentState.full (Coercionops.coercions ()) in
     red_flags:=
     CClosure.RedFlags.red_add_transparent
       CClosure.betaiotazeta
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 9f6fe0e651..d8dbf2f3dc 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -370,14 +370,14 @@ let coerce_search_pattern_to_sort hpat =
   let filter_head, coe_path =
     try
       let _, cp =
-        Classops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in
+        Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in
       warn ();
       true, cp
     with _ -> false, [] in
   let coerce hp coe_index =
-    let coe_ref = coe_index.Classops.coe_value in
+    let coe_ref = coe_index.Coercionops.coe_value in
     try
-      let n_imps = Option.get (Classops.hide_coercion coe_ref) in
+      let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in
       mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
     with Not_found | Option.IsNone ->
     errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc ()
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f0e73bdb29..c980d204ca 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -27,7 +27,7 @@ open EConstr
 open Vars
 open Reductionops
 open Pretype_errors
-open Classops
+open Coercionops
 open Evarutil
 open Evarconv
 open Evd
diff --git a/pretyping/classops.ml b/pretyping/coercionops.ml
index 16021b66f8..16021b66f8 100644
--- a/pretyping/classops.ml
+++ b/pretyping/coercionops.ml
diff --git a/pretyping/classops.mli b/pretyping/coercionops.mli
index 9f633843eb..9f633843eb 100644
--- a/pretyping/classops.mli
+++ b/pretyping/coercionops.mli
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0364e1b61f..bfdb471c46 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1326,7 +1326,7 @@ let understand_ltac flags env sigma lvar kind c =
   (sigma, c)
 
 let path_convertible env sigma i p q =
-  let open Classops in
+  let open Coercionops in
   let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
   let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
   let mkGApp(rt,rtl)      = DAst.make @@ Glob_term.GApp(rt,rtl) in
@@ -1379,4 +1379,4 @@ let path_convertible env sigma i p q =
       let _ = Evarconv.unify_delay env sigma tp tq in true
   with Evarconv.UnableToUnify _ | PretypeError _ -> false
 
-let _ = Classops.install_path_comparator path_convertible
+let _ = Coercionops.install_path_comparator path_convertible
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 7e140f4399..07154d4e03 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -26,7 +26,7 @@ Constr_matching
 Tacred
 Typeclasses_errors
 Typeclasses
-Classops
+Coercionops
 Program
 Coercion
 Detyping
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 8a403e5a03..625ffb5a06 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let () = Classes.declare_instance env sigma None true r in
-  let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
+  let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false in
   ()
 
 let instance_of_univ_entry = function
@@ -65,7 +65,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
     | Declare.ImportNeedQualified -> true
     | Declare.ImportDefaultBehavior -> false
   in
-  let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
+  let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in
   let inst = instance_of_univ_entry univs in
   (gr,inst)
 
diff --git a/vernac/class.ml b/vernac/comCoercion.ml
index 3c43b125d1..56ab6f289d 100644
--- a/vernac/class.ml
+++ b/vernac/comCoercion.ml
@@ -18,7 +18,7 @@ open Context
 open Vars
 open Termops
 open Environ
-open Classops
+open Coercionops
 open Declare
 open Libobject
 
@@ -231,7 +231,7 @@ let check_source = function
 let cache_coercion (_,c) =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  Classops.declare_coercion env sigma c
+  Coercionops.declare_coercion env sigma c
 
 let open_coercion i o =
   if Int.equal i 1 then
diff --git a/vernac/class.mli b/vernac/comCoercion.mli
index 3254d5d981..f98ef4fdd6 100644
--- a/vernac/class.mli
+++ b/vernac/comCoercion.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 open Names
-open Classops
+open Coercionops
 
 (** Classes and coercions. *)
 
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index b603c54026..8de1c69424 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -553,7 +553,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
+  List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index eb7b28f15b..d04a02febc 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -199,7 +199,7 @@ let print_opacity ref =
 (*******************)
 
 let print_if_is_coercion ref =
-  if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+  if Coercionops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
 
 (*******************)
 (* *)
@@ -951,7 +951,7 @@ let inspect env sigma depth =
 (*************************************************************************)
 (* Pretty-printing functions coming from classops.ml                     *)
 
-open Classops
+open Coercionops
 
 let print_coercion_value v = Printer.pr_global v.coe_value
 
@@ -965,7 +965,7 @@ let print_path ((i,j),p) =
     str"] : ") ++
   print_class i ++ str" >-> " ++ print_class j
 
-let _ = Classops.install_path_printer print_path
+let _ = Coercionops.install_path_printer print_path
 
 let print_graph () =
   prlist_with_sep fnl print_path (inheritance_graph())
diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli
index dc4280f286..2ee9c4ed33 100644
--- a/vernac/prettyp.mli
+++ b/vernac/prettyp.mli
@@ -52,7 +52,7 @@ val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
 val print_graph : unit -> Pp.t
 val print_classes : unit -> Pp.t
 val print_coercions : unit -> Pp.t
-val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
 val print_canonical_projections : env -> Evd.evar_map -> Pp.t
 
 (** Pretty-printing functions for type classes and instances *)
diff --git a/vernac/record.ml b/vernac/record.ml
index ea10e06d02..df9b4a0914 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -366,8 +366,8 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
             let refi = GlobRef.ConstRef kn in
             Impargs.maybe_declare_manual_implicits false refi impls;
             if flags.pf_subclass then begin
-              let cl = Class.class_of_global (GlobRef.IndRef indsp) in
-                Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
+              let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
+                ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
             end;
             let i = if is_local_assum decl then i+1 else i in
               (Some kn::sp_projs, i, Projection term::subst)
@@ -489,7 +489,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
     let cstr = (rsp, 1) in
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = GlobRef.ConstructRef cstr in
-    let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in
+    let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in
     let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
     rsp
   in
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 5226c2ba65..7b4924eaed 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -21,7 +21,7 @@ RecLemmas
 Library
 Prettyp
 Lemmas
-Class
+ComCoercion
 Auto_ind_decl
 Search
 Indschemes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 439ec61d38..604d1b28ff 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -49,9 +49,9 @@ let get_goal_or_global_context ~pstate glnum =
   | Some p -> Pfedit.get_goal_context p glnum
 
 let cl_of_qualid = function
-  | FunClass -> Classops.CL_FUN
-  | SortClass -> Classops.CL_SORT
-  | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r)
+  | FunClass -> Coercionops.CL_FUN
+  | SortClass -> Coercionops.CL_SORT
+  | RefClass r -> ComCoercion.class_of_global (Smartlocate.smart_global ~head:true r)
 
 let scope_class_of_qualid qid =
   Notation.scope_class_of_class (cl_of_qualid qid)
@@ -524,11 +524,11 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
 
 let vernac_definition_hook ~local ~poly = let open Decls in function
 | Coercion ->
-  Some (Class.add_coercion_hook ~poly)
+  Some (ComCoercion.add_coercion_hook ~poly)
 | CanonicalStructure ->
   Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
 | SubClass ->
-  Some (Class.add_subclass_hook ~poly)
+  Some (ComCoercion.add_subclass_hook ~poly)
 | _ -> None
 
 let fresh_name_for_anonymous_theorem () =
@@ -1034,7 +1034,7 @@ let vernac_coercion ~atts ref qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
-  Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
+  ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
   Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion ~atts id qids qidt =
@@ -1042,7 +1042,7 @@ let vernac_identity_coercion ~atts id qids qidt =
   let local = enforce_locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  Class.try_add_new_identity_coercion id ~local ~poly ~source ~target
+  ComCoercion.try_add_new_identity_coercion id ~local ~poly ~source ~target
 
 (* Type classes *)