diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-02-22 20:08:52 -0800 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-03-30 17:48:17 -0700 |
| commit | ef6202218c92bf3fb5bcdeca0c372e5d124cd537 (patch) | |
| tree | 0088016d1a47d56c3f8c1825144e3ccba01aaccd /vernac/vernacentries.ml | |
| parent | 0fa8b8cb53050d48187fd2577f2fef0f1a45d024 (diff) | |
Remove deprecated commands Arguments Scope and Implicit Arguments
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 5 |
1 files changed, 1 insertions, 4 deletions
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 _ |