diff options
| author | Arnaud Spiwack | 2014-10-22 10:55:52 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-22 13:44:57 +0200 |
| commit | d856e6ea6366e148b9b215fc1ef9631c1da07320 (patch) | |
| tree | 7ea6b798e5eae3e7bdeb7959f90677baed703b9e | |
| parent | 2592ea6490cdf799432260c99a934605a2739849 (diff) | |
CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defined names in term binders.
Closes #3747.
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -185,7 +185,10 @@ Tactics the relevant hypotheses). - New construct "uconstr:c" and "type_term c" to build untyped terms. - Binders in terms defined in Ltac (either "constr" or "uconstr") can - now take their names from identifier defined in Ltac. + now take their names from identifier defined in Ltac. As a + consequence, a name cannot be used in a binder (constr:(fun x => + ...)) if an Ltac variable of that name already exists and does not + contain an identifier. Source of occasional incompatibilities. - The "refine" tactic now accepts untyped terms built with "uconstr" so that terms with holes can be constructed piecewise in Ltac. - New bullets --, ++, **, ---, +++, ***, ... made available. |