diff options
Diffstat (limited to 'grammar/tacextend.mlp')
| -rw-r--r-- | grammar/tacextend.mlp | 72 |
1 files changed, 0 insertions, 72 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp deleted file mode 100644 index a093f78388..0000000000 --- a/grammar/tacextend.mlp +++ /dev/null @@ -1,72 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** WARNING: this file is deprecated; consider modifying coqpp instead. *) - -(** Implementation of the TACTIC EXTEND macro. *) - -open Q_util -open Argextend - -let plugin_name = <:expr< __coq_plugin_name >> - -let rec mlexpr_of_clause = function -| [] -> <:expr< TyNil >> -| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> -| ExtNonTerminal (g, _) :: cl -> - <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> - -open Pcaml - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "TACTIC"; "EXTEND"; s = tac_name; - depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ]; - level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ]; - OPT "|"; l = LIST1 tacrule SEP "|"; - "END" -> - let level = match level with Some i -> int_of_string i | None -> 0 in - let level = mlexpr_of_int level in - let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in - let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in - declare_str_items loc [ <:str_item< Tacentries.tactic_extend - $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation = - $depr$ } $l$ >> ] ] ] - ; - tacrule: - [ [ "["; l = LIST1 tacargs; "]"; - "->"; "["; e = Pcaml.expr; "]" -> - let e = <:expr< fun ist -> $e$ >> in - <:expr< TyML($mlexpr_of_clause l$, $binders_of_tokens e l$) >> - ] ] - ; - - tacargs: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, Some s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, Some s) - | e = LIDENT -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, None) - | s = STRING -> - let () = if s = "" then failwith "Empty terminal." in - ExtTerminal s - ] ] - ; - tac_name: - [ [ s = LIDENT -> s - | s = UIDENT -> s - ] ] - ; - END |