diff options
Diffstat (limited to 'parsing/extend.ml4')
| -rw-r--r-- | parsing/extend.ml4 | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/parsing/extend.ml4 b/parsing/extend.ml4 index 515cdd9790..1e2a00ccec 100644 --- a/parsing/extend.ml4 +++ b/parsing/extend.ml4 @@ -8,23 +8,6 @@ open Pcoq open Coqast open Ast -(* Done here to get parsing/g_*.ml4 non dependent from kernel *) -let constr_parser_with_glob = map_entry Astterm.globalize_ast Constr.constr -let tactic_parser_with_glob = map_entry Astterm.globalize_ast Tactic.tactic -let vernac_parser_with_glob = map_entry Astterm.globalize_ast Vernac.vernac - -(* This updates default parsers for Grammar actions and Syntax *) -(* patterns by inserting globalization *) -let _ = update_constr_parser constr_parser_with_glob -let _ = update_tactic_parser tactic_parser_with_glob -let _ = update_vernac_parser vernac_parser_with_glob - -(* This installs default quotations parsers to escape the ast parser *) -(* "constr" is used by default in quotations found in the ast parser *) -let _ = define_quotation true "constr" constr_parser_with_glob -let _ = define_quotation false "tactic" tactic_parser_with_glob -let _ = define_quotation false "vernac" vernac_parser_with_glob - (* Converting and checking grammar command *) type nonterm = |