diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 00dc19332..d447a97e8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1860,7 +1860,7 @@ let subst_induction_arg subst = function let subst_evaluable_reference subst = function | EvalVarRef id -> EvalVarRef id - | EvalConstRef kn -> EvalConstRef (subst_kn subst kn) + | EvalConstRef kn -> EvalConstRef (subst_con subst kn) let subst_and_short_name f (c,n) = assert (n=None); (* since tacdef are strictly globalized *) |