Age | Commit message (Collapse) | Author | Files | Lines |
|
|
|
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...
|
|
by applying the patch distributed by the coq team
Bump PKGREVISION, and require ocaml >= 3.09
|
|
USE_GNU_TOOLS -> USE_TOOLS
awk -> gawk
m4 -> gm4
make -> gmake
sed -> gsed
yacc -> bison
|
|
|
|
|
|
- Initial patches supplied by Antoine Reilles, thanks !
- Lots of changes/fixes/updates, see: CHANGES
|
|
packages: ocaml, ocaml-graphics and labltk. Bump PKGREVISION.
|
|
Suggested by Roland Illig, ok'd by various.
|
|
in the process. (More information on tech-pkg.)
Bump PKGREVISION and BUILDLINK_DEPENDS of all packages using libtool and
installing .la files.
Bump PKGREVISION (only) of all packages depending directly on the above
via a buildlink3 include.
|
|
|
|
|
|
which now includes powerpc and sparc.
Bump PKGREVISION.
|
|
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.
|