diff options
| author | Pierre-Marie Pédrot | 2014-05-22 00:58:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-22 01:03:44 +0200 |
| commit | 9c927ebdd7e72bb4ae39b549f55f375d66683be5 (patch) | |
| tree | 3952c62a17e4b73986d5f2bb52034cd8ae57fa6e /parsing/g_tactic.ml4 | |
| parent | cfd8ec82784a5c893b63f3c82736eb76fe487ad7 (diff) | |
Removing useless use of metaids in tactic AST.
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 |
1 files changed, 1 insertions, 4 deletions
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) ] ] |