18 Commits

Author SHA1 Message Date
daniel
0cedcb5459 Repair coq on non-native archs as pointed out by MAINTAINER and also
by recent !native bulk builds.

In particular:
- ocaml-num is needed at runtime, not just at build-time.
- packing list was incorrect, preventing packaging.

Compile tested by cwen@ on powerpc, and by jj@ on mips64. Some basic
runtime tests by myself on powerpc.
2020-09-16 21:13:09 +00:00
daniel
baac4a0e6e Update to coq 8.12.0; tested by myself and MAINTAINER on amd64. 2020-08-09 02:45:34 +00:00
chrisz
5ae518c3da Upgrade math/coq to 8.11.1
ok daniel@
2020-06-01 06:04:50 +00:00
chrisz
55f72cd4c1 fix plist for bytecode-only arm64, sparc64
OK jca@
2019-10-07 06:40:15 +00:00
daniel
e14e5d002f - Update to beta3 to pickup a few bug fixes.
- Make the regression tests more verbose like we used but lost in one
  of the recent updates.

ok Yozo Toda (MAINTAINER)
2019-09-20 03:28:33 +00:00
chrisz
3eeef006f1 Upgrade to 8.10beta2, which supports OCaml 4.08.
no objections krw@, please commit daniel@
2019-09-06 22:10:18 +00:00
chrisz
b438efbd00 Upgrade OCaml and dependent ports
testing and OKs by avsm@, jca@, krw@ Thanks a lot !
2019-03-04 12:51:12 +00:00
espie
0ac561f238 this does need the emacs dirs 2018-05-20 08:25:36 +00:00
naddy
b565ffc051 g/c PFRAG.shared from OCaml ports; ok chrisz@ 2016-03-29 11:27:00 +00:00
daniel
1c147d96fd Update to coq 8.4pl6; ok Yozo (MAINTAINER), sthen@ 2015-06-19 21:25:32 +00:00
daniel
090ffc6b18 Update to 8.4pl3; Yozo Toda.
ok sthen@
2014-03-26 03:27:26 +00:00
sthen
7d0c407ab6 update to coq 8.4pl2, from Daniel Dickman, ok Yozo TODA (maintainer) 2013-11-08 23:11:48 +00:00
chrisz
cc072d54cf update to version 8.4
OK
jasper@, sthen@, Yozo Toda (maintainer)
2013-01-04 11:07:28 +00:00
espie
d7c7e778ad new style PLISTs 2004-09-15 09:11:58 +00:00
naddy
2276d3b230 remove WWW lines 2003-12-15 21:42:08 +00:00
sturm
18ebc748c1 make coq use the ocaml module
requested by and OK naddy@
2002-12-18 09:40:07 +00:00
naddy
6cfb0e81a0 Update to 7.3.1 and unbreak.
From: Yozo Toda <yozo@v007.vaio.ne.jp>
2002-11-04 21:10:44 +00:00
naddy
3367255cb4 Import of coq 7.0.
Submitted by Yozo Toda <yozo@imit.chiba-u.ac.jp>.

The Coq Proof Assistant is designed to write formal specifications, programs
and to verify that programs are correct with respect to their specification.
2001-09-22 14:24:31 +00:00