From ad7bec4eacfc3255f7270feab55eca407ac8766c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 24 Oct 2000 09:00:37 +0000
Subject: Meilleur endroit pour déclarer les parseurs de grammaires et joli
 affichage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@749 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ce7c4f1d05..e0ccdc6e4d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -16,6 +16,23 @@ open Summary
  **** PRETTY-PRINTING ****
  *************************)
 
+(* Done here to get parsing/g_*.ml4 non dependent from kernel *)
+let constr_parser_with_glob = map_entry Astterm.globalize_constr 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
+
 (* Pretty-printer state summary *)
 let _ = 
   declare_summary "syntax"
-- 
cgit v1.2.3