diff options
| author | Hugo Herbelin | 2014-10-13 16:08:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-13 16:10:50 +0200 |
| commit | c8ca44cf328746636865834843744fea6f73d0d2 (patch) | |
| tree | 96db7ea003d987bfb112aec2e9d64ae82f7e1cff /CHANGES | |
| parent | 7e8b7bc5fd911d2fb34eecd238788fc2e81afa0f (diff) | |
Mentioning incompatibility shown in #3718 and coming from #3050
(interpreting "match goal"'s hypotheses in scope %type).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 4 insertions, 3 deletions
@@ -36,7 +36,6 @@ Logic - New option -type-in-type to collapse the universe hierarchy (this makes the logic inconsistent). - Vernacular commands - A command "Variant" allows to define non-recursive variant types. @@ -146,15 +145,17 @@ Tactics behaves like if matching on "?X pat1 ... patn", i.e. accepting "_" to be instantiated by an applicative term (experimental at this stage, potential source of incompatibilities). +- In Ltac matching on goal, types of hypotheses are now interpreted in + the %type scope (possible source of incompatibilities). - "change ... in ..." and "simpl ... in ..." now consider nested occurrences (possible source of incompatibilities since this alters the numbering of occurrences). - The "change p with c" tactic semantics changed, now typechecking "c" at each matching occurrence "t" of the pattern "p", and converting "t" with "c". -- Now "appcontext" and "context" behave the same. The old buggy behaviour of +- Now "appcontext" and "context" behave the same. The old buggy behavior of "context" can be retrieved at parse time by setting the - "Tactic Compat Context" flag. (possible source of incompatibilities). + "Tactic Compat Context" flag (possible source of incompatibilities). - New introduction pattern p/c which applies lemma c on the fly on the hypothesis under consideration before continuing with introduction pattern p. - New introduction pattern [= x1 .. xn] applies "injection as [x1 .. xn]" |