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
---
 vernac/comAssumption.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comAssumption.ml')

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