diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index d77349bc58..c017393c1b 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -302,7 +302,6 @@ type vernac_expr = | VernacRestoreState of string (* Resetting *) - | VernacRemoveName of lident | VernacResetName of lident | VernacResetInitial | VernacBack of int |