diff options
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -216,6 +216,8 @@ Tactics on the fly if injection is applicable to the hypothesis under consideration (idea borrowed from Georges Gonthier). Introduction pattern [=] applies "discriminate" if a discriminable equality. +- New introduction patterns * and ** to respectively introduce all forthcoming + dependent variables and all variables/hypotheses dependent or not. - Tactic "injection c as ipats" now clears c if c refers to an hypothesis and moves the resulting equations in the hypotheses independently of the number of ipats, which has itself to be less |