diff options
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -18,12 +18,15 @@ Syntax translator - Unsafe for annotation Cases when constructors coercions are used or when annotations are eta-reduced predicates - Recursive keyword set by default (and no longer needed) in Tactic Definition +- Notation for record projection Syntax for arithmetic - Notation "=" and "<>" in Z and R are no longer implicitly in Z or R (with possible introduction of a coercion), use <Z>...=... or <Z>...<>... instead +- "inject_nat" renamed into "INZ"; "INZ" from Reals do not longer exist +- Locate applied to symbols also searches for substrings Vernacular commands @@ -67,6 +70,7 @@ Tactic language - Fail tactic now accepts a failure message - New primitive tactic "FreshId" to generate new names +- Debugger prints levels of calls Tactics |