diff options
Diffstat (limited to 'tactics/tacticMatching.ml')
| -rw-r--r-- | tactics/tacticMatching.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml index 85108f8ed..b11841a65 100644 --- a/tactics/tacticMatching.ml +++ b/tactics/tacticMatching.ml @@ -215,9 +215,6 @@ module PatternMatching (E:StaticEnvironment) = struct (** Declares a substitution. *) let put_subst subst : unit m = put subst empty_context_subst empty_term_subst - (** Declares a context substitution. *) - let put_context context : unit m = put empty_subst context empty_term_subst - (** Declares a term substitution. *) let put_terms terms : unit m = put empty_subst empty_context_subst terms |