Merge PR #11293: Rename files with Class in their name to make their role clearer.

5 files changed, 4 insertions, 4 deletions

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