From cc3ded87f0f440eac2746d59b7aeba60ca9f691f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 Dec 2019 11:41:33 +0100
Subject: 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
---
 pretyping/pretyping.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/pretyping.ml')

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
-- 
cgit v1.2.3