diff options
| author | Hugo Herbelin | 2019-12-23 22:57:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-23 22:57:20 +0100 |
| commit | 028d64fb5c461e32752b0f8a92d4e2eca2a26d0d (patch) | |
| tree | 8380a901d2c066536f38552f67ffa76f0e3364b3 /pretyping/pretyping.ml | |
| parent | 3b9763487f96d308f6339c7eb4fc834b069f6e40 (diff) | |
| parent | cc3ded87f0f440eac2746d59b7aeba60ca9f691f (diff) | |
Merge PR #11293: Rename files with Class in their name to make their role clearer.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |