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
---
 dev/base_include | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev/base_include')

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