diff options
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 42e61cb57e..afffaffbe9 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -27,9 +27,8 @@ let subst_quantified_hypothesis _ x = x let subst_declared_or_quantified_hypothesis _ x = x -let subst_glob_constr_and_expr subst (c,e) = - assert (Option.is_empty e); (* e<>None only for toplevel tactics *) - (Detyping.subst_glob_constr subst c,None) +let subst_glob_constr_and_expr subst (c, e) = + (Detyping.subst_glob_constr subst c, e) let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) |