diff options
| author | Pierre-Marie Pédrot | 2015-02-27 14:05:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-27 14:07:15 +0100 |
| commit | 9fea58122001535bdee63317b56f2afb727167c7 (patch) | |
| tree | d78f84e01a6d1c11273abe3e5f86ce9d61dc8ab9 | |
| parent | dbdf0648f4588d812a20ea4ba7d3e866f024073c (diff) | |
Somehow fixing bug #3467.
The notations using tactics in term seem now not to respect globalized names.
It is not obvious that this is the expected behaviour, but at least it does
not die with an anomaly.
| -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 *) |