diff options
| -rw-r--r-- | tactics/tacinterp.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 8d8d12fb40..0e6760b318 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -94,9 +94,6 @@ 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 |