diff options
| -rw-r--r-- | CHANGES | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -533,6 +533,9 @@ Tactics - Behavior of introduction patterns -> and <- made more uniform (hypothesis is cleared, rewrite in hypotheses and conclusion and erasing the variable when rewriting a variable). +- New experimental option "Set Standard Proposition Elimination Names" + so that case analysis or induction on schemes in Type containing + propositions now produces "H"-based names. - Tactics from plugins are now active only when the corresponding module is imported (source of incompatibilities, solvable by adding an "Import"; in the particular case of Omega, use "Require Import OmegaTactic"). @@ -1071,9 +1074,6 @@ Other tactics clears (resp. reverts) H and all the hypotheses that depend on H. - Ltac's pattern-matching now supports matching metavariables that depend on variables bound upwards in the pattern. -- New experimental option "Set Standard Proposition Elimination Names" - so that case analysis or induction on schemes in Type containing - propositions now produces "H"-based names. Tactic definitions |