aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/vernacexpr.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index df061bfb7..dc1110ad8 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -457,8 +457,6 @@ type nonrec vernac_expr =
| VernacCheckGuard
| VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
| VernacProofMode of string
- (* Toplevel control *)
- | VernacToplevelControl of exn
(* For extension *)
| VernacExtend of extend_name * Genarg.raw_generic_argument list