From ef6202218c92bf3fb5bcdeca0c372e5d124cd537 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Thu, 22 Feb 2018 20:08:52 -0800
Subject: Remove deprecated commands Arguments Scope and Implicit Arguments

---
 intf/vernacexpr.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index dc1110ad86..96b4a0e26f 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -409,8 +409,6 @@ type nonrec vernac_expr =
   | VernacHints of string list * hints_expr
   | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
       onlyparsing_flag
-  | VernacDeclareImplicits of reference or_by_notation *
-      (explicitation * bool * bool) list list
   | VernacArguments of reference or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *
         (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
@@ -418,8 +416,6 @@ type nonrec vernac_expr =
         [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
           `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
           `DefaultImplicits ] list
-  | VernacArgumentsScope of reference or_by_notation *
-      scope_name option list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option
   | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
-- 
cgit v1.2.3