diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-25 19:25:42 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-25 19:25:42 +0000 |
| commit | 10621555f900d25df4fd2f71b045a050f8eb9f90 (patch) | |
| tree | f1b173e44dabcf1810fbc733b2a020aa0dfb3a85 /parsing/q_util.ml4 | |
| parent | 2c6c48388fa5ce84d66eb92fd9574951628a2c34 (diff) | |
Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands
It is quite nasty to insert those open in places where they can change
the semantics of surrounding code... instead, prefer using
fully-qualified names in generated code when possible. For
ExtraArgType, simulate a "open Extrawit in ..." (which does exist
primitively in OCaml >= 3.12) with the usual encoding.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13759 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/q_util.ml4')
| -rw-r--r-- | parsing/q_util.ml4 | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 3a3070115..91ab29f1d 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -52,19 +52,18 @@ let mlexpr_of_option f = function | Some e -> <:expr< Some $f e$ >> open Vernacexpr -open Pcoq open Genarg let rec mlexpr_of_prod_entry_key = function - | Alist1 s -> <:expr< Alist1 $mlexpr_of_prod_entry_key s$ >> - | Alist1sep (s,sep) -> <:expr< Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Alist0 s -> <:expr< Alist0 $mlexpr_of_prod_entry_key s$ >> - | Alist0sep (s,sep) -> <:expr< Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Aopt s -> <:expr< Aopt $mlexpr_of_prod_entry_key s$ >> - | Amodifiers s -> <:expr< Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Aself -> <:expr< Aself >> - | Anext -> <:expr< Anext >> - | Atactic n -> <:expr< Atactic $mlexpr_of_int n$ >> - | Agram s -> Util.anomaly "Agram not supported" - | Aentry ("",s) -> <:expr< Agram (Gram.Entry.obj $lid:s$) >> - | Aentry (u,s) -> <:expr< Aentry $str:u$ $str:s$ >> + | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> + | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> + | Pcoq.Alist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >> + | Pcoq.Alist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> + | Pcoq.Aopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> + | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> + | Pcoq.Aself -> <:expr< Pcoq.Aself >> + | Pcoq.Anext -> <:expr< Pcoq.Anext >> + | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >> + | Pcoq.Agram s -> Util.anomaly "Agram not supported" + | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >> + | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> |