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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | pretyping/coercionops.ml (renamed from pretyping/classops.ml) | 0 | ||||
| -rw-r--r-- | pretyping/coercionops.mli (renamed from pretyping/classops.mli) | 0 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 2 |
5 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f0e73bdb29..c980d204ca 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -27,7 +27,7 @@ open EConstr open Vars open Reductionops open Pretype_errors -open Classops +open Coercionops open Evarutil open Evarconv open Evd diff --git a/pretyping/classops.ml b/pretyping/coercionops.ml index 16021b66f8..16021b66f8 100644 --- a/pretyping/classops.ml +++ b/pretyping/coercionops.ml diff --git a/pretyping/classops.mli b/pretyping/coercionops.mli index 9f633843eb..9f633843eb 100644 --- a/pretyping/classops.mli +++ b/pretyping/coercionops.mli diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0364e1b61f..bfdb471c46 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1326,7 +1326,7 @@ let understand_ltac flags env sigma lvar kind c = (sigma, c) let path_convertible env sigma i p q = - let open Classops in + let open Coercionops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in @@ -1379,4 +1379,4 @@ let path_convertible env sigma i p q = let _ = Evarconv.unify_delay env sigma tp tq in true with Evarconv.UnableToUnify _ | PretypeError _ -> false -let _ = Classops.install_path_comparator path_convertible +let _ = Coercionops.install_path_comparator path_convertible diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 7e140f4399..07154d4e03 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -26,7 +26,7 @@ Constr_matching Tacred Typeclasses_errors Typeclasses -Classops +Coercionops Program Coercion Detyping |