diff options
| author | Emilio Jesus Gallego Arias | 2020-05-20 00:47:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | d83e95cce852c5471593a27d0fdca39a262c885f (patch) | |
| tree | 9117298b6f6d0a69e6863578858de27ddb23e8ba /vernac/vernac.mllib | |
| parent | 7d183d8a12a03a608a3dc8a724142468b45886ac (diff) | |
[declare] [api] Removal of deprecated functions
The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.
All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
Diffstat (limited to 'vernac/vernac.mllib')
| -rw-r--r-- | vernac/vernac.mllib | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index c30703d734..78f9b6098a 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -44,6 +44,3 @@ ComArguments Vernacentries Vernacstate Vernacinterp -Proof_global -Pfedit -DeclareDef |