0cf71c7231
Bug fixes - Solved bugs : #2851 #2863 #2865 #2893 #2895 #2892 #2905 #2906 #2907 #2917 #2921 #2930 #2941 #2878 - Partially fixed bug : #2904 - Various fixes concerning coq_makefile Optimizations - "Union by rank" optimization for universes contributed by J.H. Jourdan and G. Sherrer (see union-find-and-coq-universes on gagallium blog). Libraries - Internal organisation of some modular libraries have slightly changed due to bug #2904 (GenericMinMax, OrdersTac) - No more constant "int" in ZArith/Int.v to avoid name clash with OCaml (cf bug #2878). Coqide - Improved shutdown of coqtop processes spawned by coqide (in particular added a missing close_on_exec primitive before forking). - On windows, launching coqide with the -debug option now produces a log file in the user's temporary directory. The location of this log file is displayed in the "About" message.
6 lines
308 B
Text
6 lines
308 B
Text
$NetBSD: distinfo,v 1.15 2013/01/22 15:32:03 jaapb Exp $
|
|
|
|
SHA1 (coq-8.4pl1.tar.gz) = 23d403dbe9e410a99c584d0210dc527950051679
|
|
RMD160 (coq-8.4pl1.tar.gz) = fa472852de474ed5b83ddd4bd5a303f32b5dba94
|
|
Size (coq-8.4pl1.tar.gz) = 4139808 bytes
|
|
SHA1 (patch-Makefile.build) = 3fa72d701a80f363ef637e3cbd0e4c2d410da6c4
|