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 /tactics | |
| parent | cfd8ec82784a5c893b63f3c82736eb76fe487ad7 (diff) | |
Removing useless use of metaids in tactic AST.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 0bb86cbf7d..7062737382 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -106,7 +106,7 @@ let intern_hyp ist (loc,id as locid) = else Pretype_errors.error_var_not_found_loc loc id -let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id) +let intern_hyp_or_metaid ist id = intern_hyp ist id let intern_or_var ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) |