diff options
| author | letouzey | 2010-11-19 10:20:05 +0000 |
|---|---|---|
| committer | letouzey | 2010-11-19 10:20:05 +0000 |
| commit | f44ddd58ffb19ad08389580c76de2130e7cd1197 (patch) | |
| tree | f8ea5e4cd4b091dd4224b61e63ee103b9ddc4502 | |
| parent | a7cfd8a9cc4148241e80b8b598f7878b308b8647 (diff) | |
CHANGES: small re-sync with the one of branch v8.3
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13653 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -20,7 +20,8 @@ Rewriting tactics proofs that are dependent (use "simple subst" for preserving compatibility). - Added support for Leibniz-rewriting of dependent hypotheses. - Renamed "Morphism" into "Proper" and "respect" into "proper_prf" - (possible source of incompatibility). + (possible source of incompatibility). A partial fix is to define + "Notation Morphism R f := (Proper (R%signature) f)." - New tactic variants "rewrite* by" and "autorewrite*" that rewrite respectively the first and all matches whose side-conditions are solved. |