As camlp5 is required with ocaml 3.10, bring it as a dependency anyway,
instead of requiring ocaml 3.10
Changes include:
* Installation
- Support for compilation with ocaml 3.10 and (transitional) camlp5.
- Many bugs have been fixed (cf coq-bugs web page)
- All known failures of ROmega have been fixed. It should now be a
faithful and quicker replacement for Omega (except when nat parts
are involved). ROmega and Omega now handle <->.
- Better computational behavior of some constants (eq_nat_dec and
le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
transparent) [exceptionally source of incompatibilities].
- Loading FSets/FMap used to open unwanted scopes of integer datatypes
(see bug #1347). These scopes may need to be manually opened now.
Many changes, among them:
- Many bugs have been fixed (cf coq-bugs web page)
- changed parsing precedence of let/in and fun constructions of Ltac:
let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
- New primitive "external" for communication with tool external to Coq.
- Omega now handles arbitrary precision integers.
- Haskell extraction: types of functions are now printed, better
unsafeCoerce mechanism, both for hugs and ghc.
- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme.
- New notation "exists! x:A, P" for unique existence.
- New library on String and Ascii characters (contributed by L. Thery).
- New library FSets+FMaps of finite sets and maps.
- New library QArith on rational numbers.
- Few improvements in ZArith potentially exceptionally breaking the
compatibility (useless hypothesys of Zgt_square_simpl and
Zlt_square_simpl removed; fixed names mentioning letter O instead of
digit 0; weaken premises in Z_lt_induction).
Changelog:
- Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0.
- The search depth argument of auto can be parameterised in the Ltac language
- Added entry constr_may_eval for tactic extensions (new syntax)
- A couple of lemmas of ZArith were renamed: O -> 0
- many bugfixes, for extraction, Ltac, tactics...
with prior art (e.g. lang/twelf).
Coq is a Proof Assistant for a Logical Framework known as the
Calculus of Inductive Constructions. It allows the interactive
construction of formal proofs, and also the manipulation of
functional programs consistently with their specifications.
