diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-31 15:06:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-31 19:10:08 +0200 |
| commit | be01deca2b8ff22505adaa66f55f005673bf2d85 (patch) | |
| tree | c0853a41fc88a860f5a835072934aba8a8e1feeb /CHANGES | |
| parent | 37f68259ab0a33c3b5b41de70b08422d9bcd3bec (diff) | |
More on injection over a projectable "existT". - Fixing syntax "injection ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -102,6 +102,10 @@ Tactics independently of the number of ipats, which has itself to be less than the number of new hypotheses (possible source of incompatibilities; former behavior obtainable by "Unset Injection L2R Pattern Order"). +- Tactic "injection" now automatically simplifies subgoals + "existT n p = exists n p'" into "p = p'" when "n" is in an inductive type for + which a decidable equality scheme has been generated with "Scheme Equality" + (possible source of incompatibilities). - New tactic "rewrite_strat" for generalized rewriting with user-defined strategies, subsumming autorewrite. - Injection can now also deduce equality of arguments of sort Prop, by using |