diff options
| author | Théo Zimmermann | 2019-06-12 14:03:37 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-12 14:03:37 +0200 |
| commit | 0ab76e968b9f3a02678ec8aa747da47f94181055 (patch) | |
| tree | 4c89a8d0e887c193979a8f61099c78c4aa6b2280 /interp/interp.mllib | |
| parent | 0d4300771e4a6a26d948872262a79695a38c7e0d (diff) | |
| parent | 26ed9cb34ea5fc84fb086644a03d016817f30a4a (diff) | |
Merge PR #10180: `deprecated` attribute support for notations and syntactic definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
Diffstat (limited to 'interp/interp.mllib')
| -rw-r--r-- | interp/interp.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/interp.mllib b/interp/interp.mllib index b65a171ef9..52978a2ab6 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,4 @@ +Deprecation NumTok Constrexpr Tactypes |