diff options
| author | Emilio Jesus Gallego Arias | 2019-04-02 13:22:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-10 01:57:54 +0200 |
| commit | 1cdaa823aa2db2f68cf63561a85771bb98aec70f (patch) | |
| tree | 4359c3c1051797f89202793e788ee145a0826521 /library/nametab.ml | |
| parent | 8ee7a4a7003fc2c5b01e0d6041961b3da14c0c84 (diff) | |
[api] Remove 8.10 deprecations.
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 95890b2edf..bd0ea5f04f 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -43,12 +43,6 @@ module GlobDirRef = struct end -type global_dir_reference = GlobDirRef.t -[@@ocaml.deprecated "Use [GlobDirRef.t]"] - -let eq_global_dir_reference = GlobDirRef.equal -[@@ocaml.deprecated "Use [GlobDirRef.equal]"] - exception GlobalizationError of qualid let error_global_not_found qid = @@ -516,10 +510,6 @@ let exists_cci sp = ExtRefTab.exists sp !the_ccitab let exists_dir dir = DirTab.exists dir !the_dirtab -let exists_section = exists_dir - -let exists_module = exists_dir - let exists_modtype sp = MPTab.exists sp !the_modtypetab let exists_universe kn = UnivTab.exists kn !the_univtab @@ -585,10 +575,3 @@ let global_inductive qid = | ref -> user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" (pr_qualid qid ++ spc () ++ str "is not an inductive type") - -(********************************************************************) - -(* Deprecated synonyms *) - -let extended_locate = locate_extended -let absolute_reference = global_of_path |