diff options
Diffstat (limited to 'plugins/ltac/tacsubst.ml')
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 918d1faeb..79bf3685e 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -121,7 +121,7 @@ let subst_raw_may_eval subst = function | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) + | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc)) | Term pc -> Term (subst_glob_constr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function |