diff options
| author | Pierre-Marie Pédrot | 2019-12-16 11:41:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-22 18:28:41 +0100 |
| commit | cc3ded87f0f440eac2746d59b7aeba60ca9f691f (patch) | |
| tree | a1c206e7edad64ee8510323b4c46fbc2b0c1528f /interp/notation.mli | |
| parent | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (diff) | |
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
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 864e500d56..ea5125f7ec 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -271,7 +271,7 @@ val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option -val scope_class_of_class : Classops.cl_typ -> scope_class +val scope_class_of_class : Coercionops.cl_typ -> scope_class (** Building notation key *) |