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 | |
| 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')
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/notation.mli | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 28f4f5aed6..cc0c1e4602 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -678,7 +678,7 @@ let remove_one_coercion inctx c = try match match_coercion_app c with | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in - (match Classops.hide_coercion r with + (match Coercionops.hide_coercion r with | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) -> (* We skip the coercion *) let l = List.skipn (n - pars) args in diff --git a/interp/notation.ml b/interp/notation.ml index 5dc1658824..93969f3718 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1430,7 +1430,7 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) -open Classops +open Coercionops type scope_class = cl_typ 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 *) |