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/comInductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comInductive.ml')

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