diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 08:59:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 08:59:59 +0000 |
| commit | 77f45845c097053b7e75135f5d1a7f8ef50bad98 (patch) | |
| tree | d4233ce94d136397432b59756e267cea0ca33092 | |
| parent | 15b296d6c496f0adde33517a774bbffa5ffcef2d (diff) | |
Bug de copier-coller
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@748 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 515cdd979..1e2a00cce 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 = |