Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 27 insertions, 0 deletions

diff --git a/ANNONCE b/ANNONCE
new file mode 100644
index 00000000..5e634f2c
--- /dev/null
+++ b/ANNONCE
@@ -0,0 +1,27 @@
+The main features of Coq version 8.1 are
+
+- the implementation of an alternative algorithm for checking the
+  convertibility of types, specially dedicated to fast type-checking
+  of reflexion-based proofs, and more generally to intensive
+  computation
+
+- richer inductive types
+
+  - support for recursively non uniform parameters
+  - support for a strong form of sort-polymorphism
+
+- improved tactics
+
+  - new implementation of setoid rewrite (contributed by C. Sacerdoti Coen)
+  - new implementation of ring (contributed by B. Grégoire and A. Mahboubi)
+  - and several other new tactic features
+
+- new libraries
+ 
+  - finite sets and finite maps (by J.-C. Filliâtre and P. Letouzey)
+  - strings (by L. Théry)
+  - significative extensions of the library on lists
+  - a few other extensions
+
+- improved module system
+