diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
3 files changed, 3 insertions, 6 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 58def67b68..f70a865d77 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -215,7 +215,7 @@ GEXTEND Gram | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] ; message_token: - [ [ id = identref -> MsgIdent (AI id) + [ [ id = identref -> MsgIdent id | s = STRING -> MsgString s | n = integer -> MsgInt n ] ] ; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 2003ec7f94..3142522023 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -228,10 +228,7 @@ GEXTEND Gram ; (* An identifier or a quotation meta-variable *) id_or_meta: - [ [ id = identref -> AI id - - (* This is used in quotations *) - | id = METAIDENT -> MetaId (!@loc, id) ] ] + [ [ id = identref -> id ] ] ; open_constr: [ [ c = constr -> ((),c) ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 810a652dc0..7d138efa3d 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -218,7 +218,7 @@ module Tactic : val red_expr : raw_red_expr Gram.entry val simple_tactic : raw_atomic_tactic_expr Gram.entry val simple_intropattern : intro_pattern_expr located Gram.entry - val clause_dft_concl : Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr Gram.entry + val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry val binder_tactic : raw_tactic_expr Gram.entry |