From ef6202218c92bf3fb5bcdeca0c372e5d124cd537 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin <jasperh@cs.washington.edu>
Date: Thu, 22 Feb 2018 20:08:52 -0800
Subject: Remove deprecated commands Arguments Scope and Implicit Arguments

---
 vernac/vernacentries.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'vernac/vernacentries.ml')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9ff4e3302..5dcc170b1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2025,7 +2025,6 @@ let interp ?proof ~atts ~st c =
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
   | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
-  | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl
   | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
   | VernacNotation (c,infpl,sc) ->
       vernac_notation ~atts c infpl sc
@@ -2099,8 +2098,6 @@ let interp ?proof ~atts ~st c =
       vernac_hints ~atts dbnames hints
   | VernacSyntacticDefinition (id,c,b) ->
       vernac_syntactic_definition ~atts id c b
-  | VernacDeclareImplicits (qid,l) ->
-      vernac_declare_implicits ~atts qid l
   | VernacArguments (qid, args, more_implicits, nargs, flags) ->
       vernac_arguments ~atts qid args more_implicits nargs flags
   | VernacReserve bl -> vernac_reserve bl
@@ -2168,7 +2165,7 @@ let check_vernac_supports_locality c l =
     | VernacDeclareMLModule _
     | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
     | VernacSyntacticDefinition _
-    | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
+    | VernacArguments _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
     | VernacSetOption _ | VernacUnsetOption _
-- 
cgit v1.2.3