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

9 files changed, 21 insertions, 21 deletions

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 *)