diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-07 18:37:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-08 19:05:05 +0100 |
| commit | b584c5529f7195849b0dd4f1eebf7c73c46f60db (patch) | |
| tree | bcb6db114e3bcea5bb0cc6fd58aa3a00a1a51334 | |
| parent | 5c23295d39da2480d83c10fe51f4201715126482 (diff) | |
Update + English in CHANGES
| -rw-r--r-- | CHANGES | 13 |
1 files changed, 7 insertions, 6 deletions
@@ -85,7 +85,7 @@ Specification Language recovered by the command "Set Asymmetric Patterns". (possible source of incompatibilities) - Type inference algorithm now granting opacity of constants. This might also - affects behavior of tactics (source of incompatibilities, solvable by + affect behavior of tactics (source of incompatibilities, solvable by re-declaring transparent constants which were set opaque). - Existential variables are now referred to by an identifier and the relevant part of their instance is displayed by default. They can be @@ -95,11 +95,11 @@ Specification Language Tactics - New tactic engine allowing dependent subgoals, fully backtracking - (aka multiple success) tactics, as well tactics which can consider - multiple goals together. In the new tactic engine, instantiation - information of existential variables is always propagated to - tactics, removing the need to manually use the "instantiate" tactics - to mark propagation points. + (also known as multiple success) tactics, as well as tactics which + can consider multiple goals together. In the new tactic engine, + instantiation information of existential variables is always + propagated to tactics, removing the need to manually use the + "instantiate" tactics to mark propagation points. * New tactical (a+b) insert a backtracking point. When (a+b);c fails during the execution of c, it can backtrack and try b instead of a. * New tactical (once a) removes all the backtracking point from a @@ -382,6 +382,7 @@ Libraries - Reals: changed definition of PI, no more axiom about sin(PI/2). - SetoidPermutation: a notion of permutation for lists modulo a setoid equality. - BigN: fixed the ocaml code doing the parsing/printing of big numbers. +- List: a couple of lemmas added especially about no-duplication, partitions. Changes from V8.4beta to V8.4beta2 ================================== |