diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-18 11:02:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-18 11:07:13 +0100 |
| commit | ca7171486839dee28732371ccde4a8bfc549368c (patch) | |
| tree | 0a72ca88a32028d1af869bcae0698e7aff9afe6f /CHANGES | |
| parent | 2e3ae20fe1ed3d7238286720c302bc892505caae (diff) | |
Hopefully the last word on having "simpl f" complying with the
semantics described in the reference manual (i.e. if "f" is a qualid,
do not add implicit arguments and, a fortiori, do not try to solve
these implicit arguments - in particular, changing DbLib which
expected this rule not to be followed).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -156,8 +156,11 @@ Tactics - "change ... in ..." and "simpl ... in ..." now properly consider nested occurrences (possible source of incompatibilities since this alters the numbering of occurrences), but do not support nested occurrences. -- simpl, vm_compute and native_compute can be given a notation string to a - constant as argument. +- Tactics simpl, vm_compute and native_compute can be given a notation string + to a constant as argument. +- When given a reference as argument, simpl, vm_compute and + native_compute now strictly interpret it as the head of a pattern + starting with this reference. - The "change p with c" tactic semantics changed, now type-checking "c" at each matching occurrence "t" of the pattern "p", and converting "t" with "c". |