diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 2 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 10 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 2 |
3 files changed, 8 insertions, 6 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 0e52dc948a..9be6c6bc4a 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -42,7 +42,7 @@ let make_act loc act pil = let make_prod_item = function | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> | ExtNonTerminal (g, _) -> - let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in + let base s = <:expr< $lid:s$ >> in mlexpr_of_prod_entry_key base g let rec make_prod = function diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index c529260e9d..53330429d9 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -61,18 +61,20 @@ let mlexpr_of_option f = function let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> +let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> + let rec mlexpr_of_prod_entry_key f = function | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> - | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> | Uentry e -> <:expr< Extend.Aentry $f e$ >> | Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> - else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >> + else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 0d4bec69d5..904662ea1c 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -106,7 +106,7 @@ let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> | ExtNonTerminal (g, id) -> let nt = type_of_user_symbol g in - let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in + let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ $mlexpr_of_prod_entry_key base g$ >> |