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 /grammar | |
| parent | cfd8ec82784a5c893b63f3c82736eb76fe487ad7 (diff) | |
Removing useless use of metaids in tactic AST.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index a52fdeb62c..cada607f67 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -83,7 +83,7 @@ let mlexpr_of_or_var f = function | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >> | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> -let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) +let mlexpr_of_hyp = (mlexpr_of_located mlexpr_of_ident) let mlexpr_of_occs = function | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >> |