diff options
| author | Pierre-Marie Pédrot | 2016-02-17 13:45:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-19 01:17:39 +0100 |
| commit | 805c8987fbb5fdeb94838bb5a3a7364c0a3d3374 (patch) | |
| tree | 847bc8e25c550394991eee31aba854667f0b60e7 /grammar | |
| parent | a99aa093b962e228817066d00f7e12698f8df73a (diff) | |
Do not export entry_key from Pcoq anymore.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 2 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 18 |
2 files changed, 10 insertions, 10 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 5bf7b65d77..bebde706e4 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -43,7 +43,7 @@ let make_act loc act pil = make (List.rev pil) let make_prod_item = function - | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >> + | ExtTerminal s -> <:expr< Extend.Atoken (Lexer.terminal $mlexpr_of_string s$) >> | ExtNonTerminal (_, g, _) -> let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in mlexpr_of_prod_entry_key base g diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 4160d03c5c..d91bfd7b8d 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -48,18 +48,18 @@ let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> let rec mlexpr_of_prod_entry_key f = function - | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> - | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key f s$ >> - | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> - | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key f s$ >> - | Extend.Uentry e -> <:expr< Pcoq.Aentry $f e$ >> + | Extend.Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Extend.Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Extend.Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Extend.Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Extend.Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Extend.Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >> + | Extend.Uentry e -> <:expr< Extend.Aentry $f e$ >> | Extend.Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (CString.equal e "tactic"); - if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> - else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + 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$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s -> |