diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index a23ce1809..c799d47e4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -97,7 +97,7 @@ val intern_hyp : val subst_genarg : substitution -> glob_generic_argument -> glob_generic_argument -val subst_rawconstr : +val subst_rawconstr_and_expr : substitution -> rawconstr_and_expr -> rawconstr_and_expr (* Interprets any expression *) |