diff options
| -rw-r--r-- | tactics/tacinterp.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 0e6760b318..8d8d12fb40 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -94,6 +94,9 @@ val intern_constr : val intern_hyp : glob_sign -> identifier Util.located -> identifier Util.located +val subst_genarg : + substitution -> glob_generic_argument -> glob_generic_argument + val subst_rawconstr : substitution -> rawconstr_and_expr -> rawconstr_and_expr |