diff options
| author | Gaëtan Gilbert | 2019-05-31 13:09:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-31 19:11:18 +0200 |
| commit | 6a5dcbbfea1af0308a4d49e7c5bcea26d74a739d (patch) | |
| tree | 8c0940a07248cf3ac0d6a62c38b1a6eef28d5629 /vernac/vernacexpr.ml | |
| parent | 04398c5fa519b742ff5b97b61bbfa0c9f9d1549c (diff) | |
Remove Show Script (deprecated in 8.10)
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index df1d08ad0f..b8946fad23 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -81,7 +81,6 @@ type locatable = type showable = | ShowGoal of goal_reference | ShowProof - | ShowScript | ShowExistentials | ShowUniverses | ShowProofNames |