head 1.39; access; symbols pkgsrc-2023Q4:1.39.0.14 pkgsrc-2023Q4-base:1.39 pkgsrc-2023Q3:1.39.0.12 pkgsrc-2023Q3-base:1.39 pkgsrc-2023Q2:1.39.0.10 pkgsrc-2023Q2-base:1.39 pkgsrc-2023Q1:1.39.0.8 pkgsrc-2023Q1-base:1.39 pkgsrc-2022Q4:1.39.0.6 pkgsrc-2022Q4-base:1.39 pkgsrc-2022Q3:1.39.0.4 pkgsrc-2022Q3-base:1.39 pkgsrc-2022Q2:1.39.0.2 pkgsrc-2022Q2-base:1.39 pkgsrc-2022Q1:1.38.0.4 pkgsrc-2022Q1-base:1.38 pkgsrc-2021Q4:1.38.0.2 pkgsrc-2021Q4-base:1.38 pkgsrc-2021Q3:1.36.0.6 pkgsrc-2021Q3-base:1.36 pkgsrc-2021Q2:1.36.0.4 pkgsrc-2021Q2-base:1.36 pkgsrc-2021Q1:1.36.0.2 pkgsrc-2021Q1-base:1.36 pkgsrc-2020Q4:1.35.0.8 pkgsrc-2020Q4-base:1.35 pkgsrc-2020Q3:1.35.0.6 pkgsrc-2020Q3-base:1.35 pkgsrc-2020Q2:1.35.0.4 pkgsrc-2020Q2-base:1.35 pkgsrc-2020Q1:1.35.0.2 pkgsrc-2020Q1-base:1.35 pkgsrc-2019Q4:1.34.0.6 pkgsrc-2019Q4-base:1.34 pkgsrc-2019Q3:1.34.0.2 pkgsrc-2019Q3-base:1.34 pkgsrc-2019Q2:1.33.0.2 pkgsrc-2019Q2-base:1.33 pkgsrc-2019Q1:1.32.0.2 pkgsrc-2019Q1-base:1.32 pkgsrc-2018Q4:1.31.0.4 pkgsrc-2018Q4-base:1.31 pkgsrc-2018Q3:1.31.0.2 pkgsrc-2018Q3-base:1.31 pkgsrc-2018Q2:1.30.0.2 pkgsrc-2018Q2-base:1.30 pkgsrc-2018Q1:1.29.0.2 pkgsrc-2018Q1-base:1.29 pkgsrc-2017Q4:1.28.0.2 pkgsrc-2017Q4-base:1.28 pkgsrc-2017Q3:1.27.0.4 pkgsrc-2017Q3-base:1.27 pkgsrc-2017Q2:1.26.0.4 pkgsrc-2017Q2-base:1.26 pkgsrc-2017Q1:1.26.0.2 pkgsrc-2017Q1-base:1.26 pkgsrc-2016Q4:1.25.0.4 pkgsrc-2016Q4-base:1.25 pkgsrc-2016Q3:1.25.0.2 pkgsrc-2016Q3-base:1.25 pkgsrc-2016Q2:1.24.0.4 pkgsrc-2016Q2-base:1.24 pkgsrc-2016Q1:1.24.0.2 pkgsrc-2016Q1-base:1.24 pkgsrc-2015Q4:1.22.0.2 pkgsrc-2015Q4-base:1.22 pkgsrc-2015Q3:1.21.0.4 pkgsrc-2015Q3-base:1.21 pkgsrc-2015Q2:1.21.0.2 pkgsrc-2015Q2-base:1.21 pkgsrc-2015Q1:1.20.0.4 pkgsrc-2015Q1-base:1.20 pkgsrc-2014Q4:1.20.0.2 pkgsrc-2014Q4-base:1.20 pkgsrc-2014Q3:1.19.0.4 pkgsrc-2014Q3-base:1.19 pkgsrc-2014Q2:1.19.0.2 pkgsrc-2014Q2-base:1.19 pkgsrc-2014Q1:1.18.0.4 pkgsrc-2014Q1-base:1.18 pkgsrc-2013Q4:1.18.0.2 pkgsrc-2013Q4-base:1.18 pkgsrc-2013Q3:1.16.0.4 pkgsrc-2013Q3-base:1.16 pkgsrc-2013Q2:1.16.0.2 pkgsrc-2013Q2-base:1.16 pkgsrc-2013Q1:1.15.0.2 pkgsrc-2013Q1-base:1.15 pkgsrc-2012Q4:1.14.0.2 pkgsrc-2012Q4-base:1.14 pkgsrc-2012Q3:1.13.0.14 pkgsrc-2012Q3-base:1.13 pkgsrc-2012Q2:1.13.0.12 pkgsrc-2012Q2-base:1.13 pkgsrc-2012Q1:1.13.0.10 pkgsrc-2012Q1-base:1.13 pkgsrc-2011Q4:1.13.0.8 pkgsrc-2011Q4-base:1.13 pkgsrc-2011Q3:1.13.0.6 pkgsrc-2011Q3-base:1.13 pkgsrc-2011Q2:1.13.0.4 pkgsrc-2011Q2-base:1.13 pkgsrc-2011Q1:1.13.0.2 pkgsrc-2011Q1-base:1.13 pkgsrc-2010Q4:1.12.0.2 pkgsrc-2010Q4-base:1.12 pkgsrc-2010Q3:1.10.0.8 pkgsrc-2010Q3-base:1.10 pkgsrc-2010Q2:1.10.0.6 pkgsrc-2010Q2-base:1.10 pkgsrc-2010Q1:1.10.0.4 pkgsrc-2010Q1-base:1.10 pkgsrc-2009Q4:1.10.0.2 pkgsrc-2009Q4-base:1.10 pkgsrc-2009Q3:1.9.0.2 pkgsrc-2009Q3-base:1.9 pkgsrc-2009Q2:1.8.0.16 pkgsrc-2009Q2-base:1.8 pkgsrc-2009Q1:1.8.0.14 pkgsrc-2009Q1-base:1.8 pkgsrc-2008Q4:1.8.0.12 pkgsrc-2008Q4-base:1.8 pkgsrc-2008Q3:1.8.0.10 pkgsrc-2008Q3-base:1.8 cube-native-xorg:1.8.0.8 cube-native-xorg-base:1.8 pkgsrc-2008Q2:1.8.0.6 pkgsrc-2008Q2-base:1.8 cwrapper:1.8.0.4 pkgsrc-2008Q1:1.8.0.2 pkgsrc-2008Q1-base:1.8 pkgsrc-2007Q4:1.7.0.2 pkgsrc-2007Q4-base:1.7 pkgsrc-2007Q3:1.6.0.6 pkgsrc-2007Q3-base:1.6 pkgsrc-2007Q2:1.6.0.4 pkgsrc-2007Q2-base:1.6 pkgsrc-2007Q1:1.6.0.2 pkgsrc-2007Q1-base:1.6 pkgsrc-2006Q4:1.5.0.8 pkgsrc-2006Q4-base:1.5 pkgsrc-2006Q3:1.5.0.6 pkgsrc-2006Q3-base:1.5 pkgsrc-2006Q2:1.5.0.4 pkgsrc-2006Q2-base:1.5 pkgsrc-2006Q1:1.5.0.2 pkgsrc-2006Q1-base:1.5 pkgsrc-2005Q4:1.3.0.8 pkgsrc-2005Q4-base:1.3 pkgsrc-2005Q3:1.3.0.6 pkgsrc-2005Q3-base:1.3 pkgsrc-2005Q2:1.3.0.4 pkgsrc-2005Q2-base:1.3 pkgsrc-2005Q1:1.3.0.2 pkgsrc-2005Q1-base:1.3 pkgsrc-2004Q4:1.1.1.1.0.10 pkgsrc-2004Q4-base:1.1.1.1 pkgsrc-2004Q3:1.1.1.1.0.8 pkgsrc-2004Q3-base:1.1.1.1 pkgsrc-2004Q2:1.1.1.1.0.6 pkgsrc-2004Q2-base:1.1.1.1 pkgsrc-2004Q1:1.1.1.1.0.4 pkgsrc-2004Q1-base:1.1.1.1 pkgsrc-2003Q4:1.1.1.1.0.2 pkgsrc-2003Q4-base:1.1.1.1 pkgsrc-base:1.1.1.1 TNF:1.1.1; locks; strict; comment @# @; 1.39 date 2022.06.21.02.21.22; author dholland; state Exp; branches; next 1.38; commitid 33KtZWGt0p2nMQID; 1.38 date 2021.10.26.10.51.32; author nia; state Exp; branches; next 1.37; commitid obtJ15s6fwznfjeD; 1.37 date 2021.10.07.14.20.48; author nia; state Exp; branches; next 1.36; commitid QJiB3Fx8Lkrv1TbD; 1.36 date 2021.02.09.22.37.43; author dholland; state Exp; branches; next 1.35; commitid bnwlxAN6i9IVq5HC; 1.35 date 2020.01.24.15.54.48; author jaapb; state Exp; branches; next 1.34; commitid 45tw63aXsHRzwXTB; 1.34 date 2019.09.01.00.51.46; author markd; state Exp; branches; next 1.33; commitid BaUf7JF1cvTscfBB; 1.33 date 2019.05.23.10.55.07; author jaapb; state Exp; branches; next 1.32; commitid uXVi5fvuyOkKMjoB; 1.32 date 2019.03.06.09.28.23; author jaapb; state Exp; branches; next 1.31; commitid RAvgSdfNiAVRNheB; 1.31 date 2018.08.02.12.57.03; author jaapb; state Exp; branches; next 1.30; commitid LxSFWWZCC4dNTxMA; 1.30 date 2018.04.09.11.29.23; author jaapb; state Exp; branches; next 1.29; commitid JTVU9gVaqtxi7LxA; 1.29 date 2018.01.10.16.26.53; author jaapb; state Exp; branches; next 1.28; commitid SYyVd1vZPj9EClmA; 1.28 date 2017.11.03.11.20.28; author jaapb; state Exp; branches; next 1.27; commitid woS4QhJBeqqI6AdA; 1.27 date 2017.09.08.17.19.01; author jaapb; state Exp; branches; next 1.26; commitid qUpimhQ87M5YTp6A; 1.26 date 2016.12.30.13.23.06; author jaapb; state Exp; branches; next 1.25; commitid q0OxTE2Kw94YG0Az; 1.25 date 2016.07.02.10.17.18; author jaapb; state Exp; branches; next 1.24; commitid lOMIBDGhyG7MtJcz; 1.24 date 2016.02.06.16.08.36; author jaapb; state Exp; branches; next 1.23; commitid TcyL81NHcysY8STy; 1.23 date 2015.12.29.06.22.54; author dholland; state Exp; branches; next 1.22; commitid hQ9FpGDp1AgBaOOy; 1.22 date 2015.11.03.22.50.33; author agc; state Exp; branches; next 1.21; commitid QD13DbDX9SeFqHHy; 1.21 date 2015.04.25.13.41.18; author jaapb; state Exp; branches; next 1.20; commitid zXAFNlWJar5jyYiy; 1.20 date 2014.10.09.22.19.01; author jaapb; state Exp; branches; next 1.19; commitid biQlkvjAMHjqNzTx; 1.19 date 2014.05.13.14.52.28; author jaapb; state Exp; branches; next 1.18; commitid VJkfJ6K2TNrv6oAx; 1.18 date 2013.10.27.22.22.31; author joerg; state Exp; branches; next 1.17; commitid Mkl81eDG270bYYax; 1.17 date 2013.10.26.19.44.33; author asau; state Exp; branches; next 1.16; commitid YqCxrijQpzD08Qax; 1.16 date 2013.04.20.08.21.49; author jaapb; state Exp; branches; next 1.15; 1.15 date 2013.01.22.15.32.03; author jaapb; state Exp; branches; next 1.14; 1.14 date 2012.10.29.11.33.17; author jaapb; state Exp; branches; next 1.13; 1.13 date 2011.03.28.20.39.26; author tonio; state Exp; branches; next 1.12; 1.12 date 2010.11.14.20.53.02; author tonio; state Exp; branches; next 1.11; 1.11 date 2010.11.07.15.39.55; author tonio; state Exp; branches; next 1.10; 1.10 date 2009.12.12.21.12.43; author asau; state Exp; branches; next 1.9; 1.9 date 2009.09.05.20.44.58; author tonio; state Exp; branches; next 1.8; 1.8 date 2008.01.12.11.48.40; author tonio; state Exp; branches; next 1.7; 1.7 date 2007.12.01.13.05.36; author tonio; state Exp; branches; next 1.6; 1.6 date 2007.02.25.15.03.52; author tonio; state Exp; branches; next 1.5; 1.5 date 2006.01.27.19.22.58; author tonio; state Exp; branches; next 1.4; 1.4 date 2006.01.16.14.34.34; author tonio; state Exp; branches; next 1.3; 1.3 date 2005.02.24.09.03.06; author agc; state Exp; branches; next 1.2; 1.2 date 2005.02.05.11.19.02; author adrianp; state Exp; branches; next 1.1; 1.1 date 2003.03.22.20.21.17; author kristerw; state Exp; branches 1.1.1.1; next ; 1.1.1.1 date 2003.03.22.20.21.17; author kristerw; state Exp; branches; next ; desc @@ 1.39 log @lang/coq: update to 8.15.2 to make it work with current ocaml. (Update during freeze ok gdt@@; even if this version might be broken, that beats definitely broken.) pkgsrc changes: use -native-compiler ondemand as recommended upstream. Now uses dune to build, and uses ocaml-zarith instead of ocaml-num. Upstream change summary: (see https://coq.github.io/doc/v8.15/refman/changes.html for the full change notes) Coq 8.15.2 fixes: - Added: intuition and dintuition use Tauto.intuition_solver (defined as auto with *) instead of hardcoding auto with *. This makes it possible to change the default solver with Ltac Tauto.intuition_solver ::= ... (#15866, fixes #7725, by Gaëtan Gilbert). - Fixed: uncaught exception UnableToUnify with bidirectionality hints (#16066, fixes #16063, by Gaëtan Gilbert). - Fixed: multiple CoqIDE bugs (#15938, fixes #15861, #15939, fixes #15882, #15964, fixes #15799, #15984, partially fixes #15873, #15996, #15912, fixes #15903, all by Jim Fehrle). -Fixed: an incorrect implementation of SFClassify, allowing for a proof of False since 8.11.0, due to Axioms present in Float.Axioms. (#16101, fixes #16096, by Ali Caglayan). Coq 8.15.1 fixes: - Fixed: cases of incompletenesses in the guard condition for fixpoints in the presence of cofixpoints or primitive projections (#15498, fixes #15451, by Hugo Herbelin). - Fixed: inconsistency when using module subtyping with squashed inductives (#15839, fixes #15838 (reported by Pierre-Marie Pédrot), by Gaëtan Gilbert). - Fixed: Check for prior declaration of a custom entry was missing for notations in only printing mode (#15628, fixes #15619, by Hugo Herbelin). - Fixed: rewrite_strat regression in 8.15.0 related to Transitive instances (#15577, fixes #15568, by Gaëtan Gilbert). - Fixed: When setoid_rewrite succeeds in rewriting at some occurrence but the resulting equality is the identity, it now tries rewriting in subterms of that occurrence instead of giving up (#15612, fixes #8080, by Gaëtan Gilbert). - Fixed: Ill-typed goals created by clearbody in the presence of transitive dependencies in the body of a hypothesis (#15634, fixes #15606, by Hugo Herbelin). - Fixed: cbn knows to refold fixpoints when Arguments with / and ! was used (#15653, fixes #15567, by Gaëtan Gilbert). - Fixed a bug where coqc -vok was not creating an empty '.vok' file. (#15745, by Ramkumar Ramachandra). - Fixed: Line numbers shown in the Errors panel of CoqIDE were incorrect; they didn't match the error locations in the script panel (#15532, fixes #15531, by Jim Fehrle). - Fixed: anomaly when using proof diffs with no focused goal (#15633, fixes #15578, by Jim Fehrle). - Fixed: Attempted edits to the processed part of a buffer while Coq is busy processing a request are now ignored to ensure "processed" highlighting is accurate (#15714, fixes #15733 and #15675 and #15725, by Jim Fehrle). - Fixed: Ensure that the names of arguments of inductive schemes are distinct so that the new Coq 8.15 preservation of argument names in the with clause of tactics in #13837 works as in Coq 8.14 for these schemes (#15537, fixes #15420, by Hugo Herbelin). Coq 8.15.0 summary: - The apply with tactic no longer renames arguments unless compatibility flag Apply With Renaming is set. - Improvements to the auto tactic family, fixing the Hint Unfold behavior, and generalizing the use of discrimination nets. - The typeclasses eauto tactic has a new best_effort option allowing it to return partial solutions to a proof search problem, depending on the mode declarations associated to each constraint. This mode is used by typeclass resolution during type inference to provide more precise error messages. - Many commands and options were deprecated or removed after deprecation and more consistently support locality attributes. - The Import command is extended with import_categories to select the components of a module to import or not, including features such as hints, coercions, and notations. - A visual Ltac debugger is now available in CoqIDE. Coq 8.14.2 fixes: - Instance warns about the default locality immediately rather than waiting until the instance is ready to be defined. This changes which command warns when the instance has a separate proof: the Instance command itself warns instead of the proof closing command (such as Defined). (#15243, fixes #14704, by Gaëtan Gilbert). Coq 8.14.1 fixes: - Fix the implementation of persistent arrays used by the VM and native compute so that it uses a uniform representation. Previously, storing primitive floats inside primitive arrays could cause memory corruption (#15081, closes #15070, by Pierre-Marie Pédrot). - Fixed missing registration of universe constraints in Module Type elaboration (#14666, fixes #14505, by Hugo Herbelin). - Fixed: abstract more robust with respect to Ltac constr bindings containing existential variables (#14671, fixes #10796, by Hugo Herbelin). - Fixed: correct support of trailing let by tactic specialize (#15046, fixes #15043, by Hugo Herbelin). - Fixed: anomaly with Extraction Conservative Types when extracting pattern-matching on singleton types (#14669, fixes #3527, by Hugo Herbelin). - Fixed: a regular error instead of an anomaly when calling Separate Extraction in a module (#14670, fixes #10796, by Hugo Herbelin). Coq 8.14.0 summary: - The internal representation of match has changed to a more space- efficient and cleaner structure, allowing the fix of a completeness issue with cumulative inductive types in the type-checker. The internal representation is now closer to the user-level view of match, where the argument context of branches and the inductive binders in and as do not carry type annotations. - A new coqnative binary performs separate native compilation of libraries, starting from a .vo file. It is supported by coq_makefile. - Improvements to typeclasses and canonical structure resolution, allowing more terms to be considered as classes or keys. - More control over notations declarations and support for primitive types in string and number notations. - Removal of deprecated tactics, notably omega, which has been replaced by a greatly improved lia, along with many bug fixes. - New Ltac2 APIs for interaction with Ltac1, manipulation of inductive types and printing. - Many changes and additions to the standard library in the numbers, vectors and lists libraries. A new signed primitive integers library Sint63 is available in addition to the unsigned Uint63 library. Coq 8.13.2: - Fixed crash when using vm_compute on an irreducible PArray.set (#14005, fixes #13998, by Guillaume Melquiond). - Fix: Never store persistent arrays as VM / native structured values. This could be used to make vo marshalling crash, and probably breaking some other invariants of the kernel (#14007, fixes #14006, by Pierre-Marie Pédrot). - Fix: Ltac2 Array.init no longer incurs exponential overhead when used recursively (#14012, fixes #14011, by Jason Gross). Coq 8.13.1: - Fix arities of VM opcodes for some floating-point operations that could cause memory corruption (#13867, by Guillaume Melquiond). - Added options -v and --version to CoqIDE (#13870, by Guillaume Melquiond). Coq 8.13.0 summary: - Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays. - Introduction of definitional proof irrelevance for the equality type defined in the SProp sort. - Cumulative record and inductive type declarations can now specify the variance of their universes. - Various bugfixes and uniformization of behavior with respect to the use of implicit arguments and the handling of existential variables in declarations, unification and tactics. - New warning for unused variables in catch-all match branches that match multiple distinct patterns. - New warning for Hint commands outside sections without a locality attribute, whose goal is to eventually remove the fragile default behavior of importing hints only when using Require. The recommended fix is to declare hints as export, instead of the current default global, meaning that they are imported through Require Import only, not Require. See the following rationale and guidelines for details. - General support for boolean attributes. - Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior. - Tactic improvements in lia and its zify preprocessing step, now supporting reasoning on boolean operators such as Z.leb and supporting primitive integers Int63. - Typing flags can now be specified per-constant / inductive. - Improvements to the reference manual including updated syntax descriptions that match Coq's grammar in several chapters, and splitting parts of the tactics chapter to independent sections. @ text @$NetBSD: distinfo,v 1.38 2021/10/26 10:51:32 nia Exp $ BLAKE2s (coq-8.15.2.tar.gz) = 5caaf97e57ce5085e965dc6e98a5e2fd5373ce3c99cbfb605a5635e8ba2f987a SHA512 (coq-8.15.2.tar.gz) = 6a5487912dedb6e54145bf3f177a091cffe13429ba2f73db7c1cc241fe10e86340c968e19cefba7d680facce55f4e914cbd16a317264b109a6f9a01ec822a8c5 Size (coq-8.15.2.tar.gz) = 7222794 bytes SHA1 (patch-Makefile.install) = ea229046833121d72db20c5b308a2e9051a68f22 SHA1 (patch-Makefile.make) = 97e809e8db8e95090b570751be92829257160b82 SHA1 (patch-tools_configure_coqide.ml) = 58956509df6ff56cbecc9c0215f6aae2b2eb3462 SHA1 (patch-tools_coqdoc_dune) = b2a1fdc3fd0bebc18754de5a0d7778e73a47c25d @ 1.38 log @lang: Replace RMD160 checksums with BLAKE2s checksums All checksums have been double-checked against existing RMD160 and SHA512 hashes The following distfiles could not be fetched (possibly fetched conditionally?): ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-aarch64-unknown-linux-gnu.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-aarch64-unknown-linux-musl.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-aarch64-unknown-netbsd.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-armv7-unknown-netbsd-eabihf.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-i686-unknown-linux-gnu.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-powerpc-unknown-netbsd90.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-sparc64-unknown-netbsd.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-x86_64-apple-darwin.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-x86_64-unknown-freebsd.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-x86_64-unknown-linux-gnu.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-x86_64-unknown-linux-musl.tar.gz ./lang/smlnj/distinfo smlnj-110.73/boot.ppc-unix.tgz ./lang/smlnj/distinfo smlnj-110.73/boot.sparc-unix.tgz ./lang/oracle-jre8/distinfo jce_policy-8.zip ./lang/oracle-jre8/distinfo jre-8u202-linux-i586.tar.gz ./lang/oracle-jre8/distinfo jre-8u202-linux-x64.tar.gz ./lang/oracle-jre8/distinfo jre-8u202-macosx-x64.tar.gz ./lang/oracle-jre8/distinfo jre-8u202-solaris-x64.tar.gz ./lang/oracle-jdk8/distinfo jdk-8u202-linux-i586.tar.gz ./lang/oracle-jdk8/distinfo jdk-8u202-linux-x64.tar.gz ./lang/oracle-jdk8/distinfo jdk-8u202-solaris-x64.tar.gz ./lang/ghc80/distinfo ghc-7.10.3-boot-x86_64-unknown-solaris2.tar.xz ./lang/ghc80/distinfo ghc-8.0.2-boot-i386-unknown-freebsd.tar.xz ./lang/ghc80/distinfo ghc-8.0.2-boot-x86_64-unknown-freebsd.tar.xz ./lang/gcc5-aux/distinfo ada-bootstrap.i386.freebsd.100B.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.i386.freebsd.84.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.x86_64.dragonfly.41.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.x86_64.freebsd.100B.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.x86_64.freebsd.84.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.x86_64.solaris.511.tar.bz2 ./lang/rust/distinfo rust-1.53.0-aarch64-apple-darwin.tar.gz ./lang/rust/distinfo rust-1.53.0-aarch64-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-1.53.0-aarch64-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-1.53.0-aarch64_be-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-1.53.0-arm-unknown-linux-gnueabihf.tar.gz ./lang/rust/distinfo rust-1.53.0-armv7-unknown-linux-gnueabihf.tar.gz ./lang/rust/distinfo rust-1.53.0-i686-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-1.53.0-powerpc-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-1.53.0-powerpc-unknown-netbsd90.tar.gz ./lang/rust/distinfo rust-1.53.0-sparc64-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-1.53.0-x86_64-apple-darwin.tar.gz ./lang/rust/distinfo rust-1.53.0-x86_64-unknown-freebsd.tar.gz ./lang/rust/distinfo rust-1.53.0-x86_64-unknown-illumos.tar.gz ./lang/rust/distinfo rust-1.53.0-x86_64-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-std-1.53.0-aarch64-apple-darwin.tar.gz ./lang/rust/distinfo rust-std-1.53.0-aarch64-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-std-1.53.0-aarch64-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-aarch64_be-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-arm-unknown-linux-gnueabihf.tar.gz ./lang/rust/distinfo rust-std-1.53.0-armv7-unknown-linux-gnueabihf.tar.gz ./lang/rust/distinfo rust-std-1.53.0-i686-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-std-1.53.0-powerpc-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-powerpc-unknown-netbsd90.tar.gz ./lang/rust/distinfo rust-std-1.53.0-sparc64-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-x86_64-apple-darwin.tar.gz ./lang/rust/distinfo rust-std-1.53.0-x86_64-unknown-freebsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-x86_64-unknown-linux-gnu.tar.gz ./lang/smlnj11072/distinfo smlnj-110.72/boot.ppc-unix.tgz ./lang/smlnj11072/distinfo smlnj-110.72/boot.sparc-unix.tgz ./lang/ghc84/distinfo ghc-8.0.2-boot-x86_64-unknown-solaris2.tar.xz ./lang/ghc84/distinfo ghc-8.4.4-boot-i386-unknown-freebsd.tar.xz ./lang/ghc84/distinfo ghc-8.4.4-boot-x86_64-apple-darwin.tar.xz ./lang/ghc84/distinfo ghc-8.4.4-boot-x86_64-unknown-freebsd.tar.xz ./lang/ghc7/distinfo ghc-7.10.3-boot-i386-unknown-freebsd.tar.xz ./lang/ghc7/distinfo ghc-7.6.3-boot-i386-unknown-solaris2.tar.xz ./lang/ghc7/distinfo ghc-7.6.3-boot-powerpc-apple-darwin.tar.xz ./lang/ghc7/distinfo ghc-7.6.3-boot-x86_64-unknown-solaris2.tar.xz ./lang/ghc90/distinfo ghc-8.10.4-boot-x86_64-unknown-solaris2.tar.xz ./lang/ghc90/distinfo ghc-9.0.1-boot-aarch64-unknown-netbsd.tar.xz ./lang/ghc90/distinfo ghc-9.0.1-boot-i386-unknown-freebsd.tar.xz ./lang/ghc90/distinfo ghc-9.0.1-boot-x86_64-apple-darwin.tar.xz ./lang/ghc90/distinfo ghc-9.0.1-boot-x86_64-unknown-freebsd.tar.xz ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk-1.7.76-freebsd-10-amd64-20150301.tar.xz ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk-1.7.76-netbsd-7-sparc64-20150301.tar.xz ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk-1.8.181-netbsd-8-aarch64-20180917.tar.xz ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk7u60-bin-dragonfly-3.6-amd64-20140719.tar.bz2 ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk7u60-bin-dragonfly-3.8-amd64-20140719.tar.bz2 ./lang/go-bin/distinfo go1.14.2.darwin-amd64.tar.gz ./lang/go-bin/distinfo go1.14.2.linux-386.tar.gz ./lang/go-bin/distinfo go1.14.2.linux-amd64.tar.gz ./lang/go-bin/distinfo go1.14.2.linux-arm64.tar.gz ./lang/go-bin/distinfo go1.14.2.linux-armv6l.tar.gz ./lang/go-bin/distinfo go1.14.2.netbsd-arm64.tar.gz ./lang/go-bin/distinfo go1.16beta1.darwin-arm64.tar.gz ./lang/gcc6-aux/distinfo ada-bootstrap.i386.freebsd.100B.tar.bz2 ./lang/gcc6-aux/distinfo ada-bootstrap.x86_64.dragonfly.41.tar.bz2 ./lang/gcc6-aux/distinfo ada-bootstrap.x86_64.freebsd.100B.tar.bz2 ./lang/gcc6-aux/distinfo ada-bootstrap.x86_64.freebsd.84.tar.bz2 ./lang/gcc6-aux/distinfo ada-bootstrap.x86_64.solaris.511.tar.bz2 ./lang/ghc810/distinfo ghc-8.8.4-boot-x86_64-unknown-solaris2.tar.xz ./lang/sun-jre7/distinfo UnlimitedJCEPolicyJDK7.zip ./lang/sun-jre7/distinfo jre-7u80-linux-x64.tar.gz ./lang/sun-jre7/distinfo jre-7u80-solaris-i586.tar.gz ./lang/sun-jre7/distinfo jre-7u80-solaris-x64.tar.gz ./lang/ghc88/distinfo ghc-8.4.4-boot-i386-unknown-freebsd.tar.xz ./lang/ghc88/distinfo ghc-8.4.4-boot-x86_64-apple-darwin.tar.xz ./lang/ghc88/distinfo ghc-8.4.4-boot-x86_64-unknown-freebsd.tar.xz ./lang/ghc88/distinfo ghc-8.4.4-boot-x86_64-unknown-solaris2.tar.xz ./lang/gcc-aux/distinfo ada-bootstrap.i386.dragonfly.36A.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.i386.freebsd.100B.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.i386.freebsd.84.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.x86_64.dragonfly.36A.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.x86_64.freebsd.100B.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.x86_64.freebsd.84.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.x86_64.solaris.511.tar.bz2 ./lang/gcc6/distinfo ecj-4.5.jar ./lang/openjdk11/distinfo bootstrap-jdk-1.11.0.7.10-netbsd-9-aarch64-20200509.tar.xz ./lang/sun-jdk7/distinfo jdk-7u80-linux-x64.tar.gz ./lang/sun-jdk7/distinfo jdk-7u80-solaris-i586.tar.gz ./lang/sun-jdk7/distinfo jdk-7u80-solaris-x64.tar.gz @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.37 2021/10/07 14:20:48 nia Exp $ d3 7 a9 5 BLAKE2s (coq-8.12.2.tar.gz) = 08bb88e3614ded682df5638971af67b3d957a86ab7ac0269bcbf6a7d8c116acd SHA512 (coq-8.12.2.tar.gz) = 6b524edbceb5795f04bbd2b52f191bfcf10b611f7a2fa0450c30b72c944f88418d261729476b64603faacfe2be5f7992a2997541e54e6f8691d4dc8b4969198d Size (coq-8.12.2.tar.gz) = 6855860 bytes SHA1 (patch-Makefile.common) = f53c41884e12bfafa825a8f27c940ab40bd9b9fe SHA1 (patch-Makefile.make) = d12827bb28e0f993908d202bfd06497cc3033699 @ 1.37 log @lang: Remove SHA1 hashes for distfiles @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.36 2021/02/09 22:37:43 dholland Exp $ d3 1 a3 1 RMD160 (coq-8.12.2.tar.gz) = d691b0fc0e0b9824f15a8a26d013f8578eb095ce @ 1.36 log @Update lang/coq to 8.12.2. Fixes build with current ocaml. Note: this update includes the import semantics fixes from 8.11 that break a lot of developments. pkgsrc change: docs build now works. Summary of changes in 8.12: Coq version 8.12 integrates many usability improvements, in particular with respect to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference manual. The main changes include: New binder notation for non-maximal implicit arguments using [ ] allowing to set and see the implicit status of arguments immediately. New notation Inductive I A | x : s := ... to distinguish the uniform from the non-uniform parameters in inductive definitions. More robust and expressive treatment of implicit inductive parameters in inductive declarations. Improvements in the treatment of implicit arguments and partially applied constants in notations, parsing of hexadecimal number notation and better handling of scopes and coercions for printing. A correct and efficient coercion coherence checking algorithm, avoiding spurious or duplicate warnings. An improved Search command which accepts complex queries. Note that this takes precedence over the now deprecated ssreflect search. Many additions and improvements of the standard library. Improvements to the reference manual include a more logical organization of chapters along with updated syntax descriptions that match Coq's grammar in most but not all chapters. Additionally, the omega tactic is deprecated in this version of Coq, and we recommend users to switch to lia in new proof scripts (see also the warning message in the corresponding chapter). Summary of changes in 8.11: The main changes brought by Coq version 8.11 are: Ltac2, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad. Primitive floats are integrated in terms and follow the binary64 format of the IEEE 754 standard, as specified in the Coq.Float.Floats library. Cleanups of the section mechanism, delayed proofs and further restrictions of template polymorphism to fix soundness issues related to universes. New unsafe flags to disable locally guard, positivity and universe checking. Reliance on these flags is always printed by Print Assumptions. Fixed bugs of Export and Import that can have a significant impact on user developments (common source of incompatibility!). New interactive development method based on vos interface files, allowing to work on a file without recompiling the proof parts of their dependencies. New Arguments annotation for bidirectional type inference configuration for reference (e.g. constants, inductive) applications. New refine attribute for Instance can be used instead of the removed Refine Instance Mode. Generalization of the under and over tactics of SSReflect to arbitrary relations. Revision of the Coq.Reals library, its axiomatisation and instances of the constructive and classical real numbers. Additionally, while the omega tactic is not yet deprecated in this version of Coq, it should soon be the case and we already recommend users to switch to lia in new proof scripts (see also the warning message in the corresponding chapter). The full (huge) changelog is here: https://coq.inria.fr/distrib/V8.12.2/refman/changes.html @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.35 2020/01/24 15:54:48 jaapb Exp $ a2 1 SHA1 (coq-8.12.2.tar.gz) = 70ba8f50fb54049fe00c5ce2c29be1c829b5297d @ 1.35 log @Updated lang/coq to version 8.10.2. Changes include: - native 63-bit machine integers; - a new sort of definitionally proof-irrelevant propositons: SProp; - private universes for opaque polymorphic constants; - string notations and numeral notations; - a new simplex-based proof engine for the tactics lia, nia, lra and nra; - new introduction patterns for SSReflect; - a tactic to rewrite under binders: under; - easy input of non-ASCII symbols in CoqIDE, which now uses GTK3. and many small improvements and bugfixes. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.32 2019/03/06 09:28:23 jaapb Exp $ d3 6 a8 5 SHA1 (coq-8.10.2.tar.gz) = ecdb79a8b4cd76912b39e037ef52545406e63799 RMD160 (coq-8.10.2.tar.gz) = a3686508b97a98b668c91a513e73f88dff02af89 SHA512 (coq-8.10.2.tar.gz) = 80df91b64efc9907480388ec479362ee21067c64436da720989d6d1645ffc2f2230ae5c13069c55842da3baa7facbd143c2190d1d64d8c87935802000a02156f Size (coq-8.10.2.tar.gz) = 6222940 bytes SHA1 (patch-Makefile.common) = 85bcb271103f87f1e1573d3856740319ee0344cd @ 1.34 log @coq: patch to build with ocaml 4.08 @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.33 2019/05/23 10:55:07 jaapb Exp $ d3 5 a7 6 SHA1 (coq-8.9.1.tar.gz) = d26646b33922bcd9eb44ef80162f8d0513784e46 RMD160 (coq-8.9.1.tar.gz) = d82a0f7d31c0e5d7b8b566cd15d7ff9f724c250b SHA512 (coq-8.9.1.tar.gz) = 66344f801b955d1b6daf3ab1d704551070c95cf9032ae74f15fb33f7ec313812b3e05c0ec277a2eb448e3fdfd9721df06d36612e2fb4928b6530d70147f1d983 Size (coq-8.9.1.tar.gz) = 6001970 bytes SHA1 (patch-Makefile.build) = 0438c2f4084dcb411bf8fdb0e513b5769d6419a7 SHA1 (patch-Makefile.common) = f232485fddc61c51cd12ac5567b706f5f2299328 @ 1.33 log @Updated lang/coq to version 8.9.1. Main changes: * some quality-of-life bug fixes, * many improvements to the documentation, * a critical bug fix related to primitive projections and native_compute, * several additional Coq libraries shipped with the Windows installer. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.32 2019/03/06 09:28:23 jaapb Exp $ d7 1 @ 1.32 log @Updated lang/coq to version 8.9.0. Many improvements and fixes, but none that appear to break compatibility. For more details see the CHANGES file. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.31 2018/08/02 12:57:03 jaapb Exp $ d3 4 a6 4 SHA1 (coq-8.9.0.tar.gz) = 8833deafd57649f875f15c0739c8ac1ffe06aeda RMD160 (coq-8.9.0.tar.gz) = b587d945a5eb0366c7a7b280f1ff08940c800a60 SHA512 (coq-8.9.0.tar.gz) = 42b2e0ae669c06803b6b527a194d78675de18869f6342fc8afc49cfc94f3e98ca0c3b4fd52d3af8c5ce66c6efb1c665ac0d65e992ad29c3f432e244f98ec2ca1 Size (coq-8.9.0.tar.gz) = 5992210 bytes @ 1.31 log @Updated package lang/coq to version 8.8.1. The list of improvements, additions, bugfixes and so on is quite large; those interested can refer to the CHANGES file in the distribution. The reference manual has been fully ported to Sphinx. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.30 2018/04/09 11:29:23 jaapb Exp $ d3 5 a7 5 SHA1 (coq-8.8.1.tar.gz) = 7dd5e31f9dd3f80d6dabfb019d1f495244f61999 RMD160 (coq-8.8.1.tar.gz) = 72b75b1d3a78c1a34b8bac86a0180b8bb677db14 SHA512 (coq-8.8.1.tar.gz) = 706fdc196ca4b8f27dae834426d926cd7d2c8b215af8cbb2653a0bda088068ed9f492cf8f11d123a1f2166b26f86e91a84765e53beb20172dc530f6dd796d8d4 Size (coq-8.8.1.tar.gz) = 5934404 bytes SHA1 (patch-Makefile.common) = d84cb2a94227e163855f35abebe71f4ec51839fc @ 1.30 log @Updated lang/coq to version 8.7.2. This fixes a critical bug in the VM handling of universes, and adds various other minor fixes and improvements. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.29 2018/01/10 16:26:53 jaapb Exp $ d3 4 a6 4 SHA1 (coq-8.7.2.tar.gz) = 0175cc658aa2c93167572a33e9e39fc63f591258 RMD160 (coq-8.7.2.tar.gz) = 2fd5c59e0143061e4253d68e8839ae3822d7a614 SHA512 (coq-8.7.2.tar.gz) = 6117ef243c62805996a21952016acaaf21db6d1b539fc813c19c897e100f45cde2bee7c9fb045b269a241b79306c656969ca8051e3212ea2090f6d7c1afad5a8 Size (coq-8.7.2.tar.gz) = 5754360 bytes @ 1.29 log @Updated package lang/coq to version 8.7.1. This is a compatibility release with OCaml 4.06.0. It also contains many bugfixes, documentation improvements and user message improvements. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.28 2017/11/03 11:20:28 jaapb Exp $ d3 4 a6 4 SHA1 (coq-8.7.1.tar.gz) = ea4c4bbed3dc1a5550bbb7e2923ed751f9ad2be6 RMD160 (coq-8.7.1.tar.gz) = 405d24ba9f0eda5b72e8bd0ed0778390cc444bf0 SHA512 (coq-8.7.1.tar.gz) = 43ef086de93bf99f94d74b9827dd16c79f4d24f5dd4332ee53bbd4588941cb602a64672638a3b3a56bfb612e4dbf7b2a3b5fd4921182dabbbe96e4fef07455b5 Size (coq-8.7.1.tar.gz) = 5671130 bytes @ 1.28 log @Updated lang/coq to version 8.7.0. Includes many improvements and bugfixes (none that seem to be breaking backwards compatibility though), see the CHANGELOG. For packaging: - camlp4 support removed, package now uses camlp5 exclusively - fix for PR pkg/52651 @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.27 2017/09/08 17:19:01 jaapb Exp $ d3 4 a6 4 SHA1 (coq-8.7.0.tar.gz) = b539e0ff6f2a6dd31bbe8856db152705f9a22a01 RMD160 (coq-8.7.0.tar.gz) = 7e752473b27a2d1a0f95ea3eb258ffba5a5a8d4f SHA512 (coq-8.7.0.tar.gz) = c806881d1ab823d9c2d748aa2d7fd3faaa0f6395536942ad214c68658b2688e6c57941947a440ddb69bf1436249067eefd866ecb1d9e4c5e774e3218c80a6fc2 Size (coq-8.7.0.tar.gz) = 5629204 bytes a7 2 SHA1 (patch-configure.ml) = 8e48a65709234281e3898ebae9041dfc04c7fe7b SHA1 (patch-ide_ideutils.ml) = 7fd59bcfc0cf4f65fd7f4e5a0ec95cb694df8417 @ 1.27 log @Updated package to latest version, 8.6.1. Changes include: - Fix #5380: Default colors for CoqIDE are actually applied. - Fix plugin warnings - Document named evars (including Show ident) - Fix Bug #5574, document function scope - Adding a test case as requested in bug 5205. - Fix Bug #5568, no dup notation warnings on repeated module imports - Fix documentation of Typeclasses eauto := - Refactor documentation of records. - Protecting from warnings while compiling 8.6 - Fixing an inconsistency between configure and configure.ml - Add test-suite checks for coqchk with constraints - Fix bug #5019 (looping zify on dependent types) - Fix bug 5550: "typeclasses eauto with" does not work with section variables. - Bug 5546, qualify datatype constructors when needed in Show Match - Bug #5535, test for Show with -emacs - Fix bug #5486, don't reverse ids in tuples - Fixing #5522 (anomaly with free vars of pat) - Fix bug #5526, don't check for nonlinearity in notation if printing only - Fix bug #5255 - Fix bug #3659: -time should understand multibyte encodings. - FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print Assumptions". - Fix outdated description in RefMan. - Repairing `Set Rewriting Schemes` - Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). - Fix description of command-line arguments for Add (Rec) LoadPath - Fix bug #5377: @@? patterns broken. - add XML protocol doc - Fix anomaly when doing [all:Check _.] during a proof. - Correction of bug #4306 - Fix #5435: [Eval native_compute in] raises anomaly. - Instances should obey universe binders even when defined by tactics. - Intern names bound in match patterns - funind: Ignore missing info for current function - Do not typecheck twice the type of opaque constants. - show unused intro pattern warning - [future] Be eager when "chaining" already resolved future values. - Opaque side effects - Fix #5132: coq_makefile generates incorrect install goal - Run non-tactic comands without resilient_command - Univs: fix bug #5365, generation of u+k <= v constraints - make `emit' tail recursive - Don't require printing-only notation to be productive - Fix the way setoid_rewrite handles bindings. - Fix for bug 5244 - set printing width ignored when given enough space - Fix bug 4969, autoapply was not tagging shelved subgoals correctly @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.26 2016/12/30 13:23:06 jaapb Exp $ d3 5 a7 5 SHA1 (coq-8.6.1.tar.gz) = 5dbaf1230c297d7c11c8715c012300a51ad80f9a RMD160 (coq-8.6.1.tar.gz) = 822b0061a99de144881b1f1166eef9e92d26de7f SHA512 (coq-8.6.1.tar.gz) = 814ab76a06ca15f927081428da74add4bc67290199fa011853b9c68a00cdefaf813b10fbac18a434f4504fce8f2173eb544080bf6f50d62caa41bb8724b13083 Size (coq-8.6.1.tar.gz) = 5588811 bytes SHA1 (patch-Makefile.common) = 79b02edff66ddcfb267816b0031c724620e67a13 d9 1 @ 1.26 log @Updated coq to latest version, 8.6. Changes include: Changes from V8.6beta1 to V8.6 ============================== Kernel - Fixed critical bug #5248 in VM long multiplication on 32-bit architectures. Was there only since 8.6beta1, so no stable release impacted. Other bug fixes in universes, type class shelving,... Changes from V8.5 to V8.6beta1 ============================== Kernel - A new, faster state-of-the-art universe constraint checker. Specification language - Giving implicit arguments explicitly to a constant with multiple choices of implicit arguments does not break any more insertion of further maximal implicit arguments. - Ability to put any pattern in binders, prefixed by quote, e.g. "fun '(a,b) => ...", "λ '(a,(b,c)), ...", "Definition foo '(x,y) := ...". It expands into a "let 'pattern := ..." Tactics - Flag "Bracketing Last Introduction Pattern" is now on by default. - Flag "Regular Subst Tactic" is now on by default: it respects the initial order of hypothesis, it contracts cycles, it unfolds no local definitions (common source of incompatibilities, fixable by "Unset Regular Subst Tactic"). - New flag "Refolding Reduction", now disabled by default, which turns on refolding of constants/fixpoints (as in cbn) during the reductions done during type inference and tactic retyping. Can be extremely expensive. When set off, this recovers the 8.4 behaviour of unification and type inference. Potential source of incompatibility with 8.5 developments (the option is set on in Compat/Coq85.v). - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract tactical w.r.t. variables appearing in the body of the proof. On by default and deprecated. Minor source of incompatibility for code relying on the precise arguments of abstracted proofs. - Serious bugs are fixed in tactic "double induction" (source of incompatibilities as soon as the inductive types have dependencies in the type of their constructors; "double induction" remains however deprecated). - In introduction patterns of the form (pat1,...,patn), n should match the exact number of hypotheses introduced (except for local definitions for which pattern can be omitted, as in regular pattern-matching). - Tactic scopes in Ltac like constr: and ltac: now require parentheses around their argument. - Every generic argument type declares a tactic scope of the form "name:(...)" where name is the name of the argument. This generalizes the constr: and ltac: instances. - When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is given a free identifier, it is not bound in subsequent tactics anymore. In order to introduce a binding, use e.g. the "fresh" primitive instead (potential source of incompatibilities). - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac. - New goal selectors. Sets of goals can be selected by listing integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24. - For uniformity with "destruct"/"induction" and for a more natural behavior, "injection" can now work in place by activating option "Structural Injection". In this case, hypotheses are also put in the context in the natural left-to-right order and the hypothesis on which injection applies is cleared. - Tactic "contradiction" (hence "easy") now also solve goals with hypotheses of the form "~True" or "t<>t" (possible source of incompatibilities because of more successes in automation, but generally a more intuitive strategy). - Option "Injection On Proofs" was renamed "Keep Proof Equalities". When enabled, injection and inversion do not drop equalities between objects in Prop. Still disabled by default. - New tactics "notypeclasses refine" and "simple notypeclasses refine" that disallow typeclass resolution when typechecking their argument, for use in typeclass hints. - Integration of LtacProf, a profiler for Ltac. - Reduction tactics now accept more fine-grained flags: iota is now a shorthand for the new flags match, fix and cofix. - The ssreflect subterm selection algorithm is now accessible to tactic writers through the ssrmatching plugin. - When used as an argument of an ltac function, "auto" without "with" nor "using" clause now correctly uses only the core hint database by default. Hints - Revised the syntax of [Hint Cut] to follow standard notation for regexps. - Hint Mode now accepts "!" which means that the mode matches only if the argument's head is not an evar (it goes under applications, casts, and scrutinees of matches and projections). - Hints can now take an optional user-given pattern, used only by [typeclasses eauto] with the [Filtered Unification] option on. Typeclasses - Many new options and new engine based on the proof monad. The [typeclasses eauto] tactic is now a multi-goal, multi-success tactic. See reference manual for more information. It is planned to replace auto and eauto in the following version. The 8.5 resolution engine is still available to help solve compatibility issues. Program - The "Shrink Obligations" flag now applies to all obligations, not only those solved by the automatic tactic. - "Shrink Obligations" is on by default and deprecated. Minor source of incompatibility for code relying on the precise arguments of obligations. Notations - "Bind Scope" can once again bind "Funclass" and "Sortclass". General infrastructure - New configurable warning system which can be controlled with the vernacular command "Set Warnings", or, under coqc/coqtop, with the flag "-w". In particular, the default is now that warnings are printed by coqc. - In asynchronous mode, Coq is now capable of recovering from errors and continue processing the document. Tools - coqc accepts a -o option to specify the output file name - coqtop accepts --print-version to print Coq and OCaml versions in easy to parse format - Setting [Printing Dependent Evars Line] can be unset to disable the computation associated with printing the "dependent evars: " line in -emacs mode - Removed the -verbose-compat-notations flag and the corresponding Set Verbose Compat vernacular, since these warnings can now be silenced or turned into errors using "-w". XML protocol - message format has changed, see dev/doc/changes.txt for more details. Many bug fixes, minor changes and documentation improvements are not mentioned here. Changes from V8.5pl2 to V8.5pl3 =============================== Critical bugfix - #4876: Guard checker incompleteness when using primitive projections Other bugfixes - #4780: Induction with universe polymorphism on was creating ill-typed terms. - #4673: regression in setoid_rewrite, unfolding let-ins for type unification. - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain. - #4769: Anomaly with universe polymorphic schemes defined inside sections. - #3886: Program: duplicate obligations of mutual fixpoints. - #4994: Documentation typo. - #5008: Use the "md5" command on OpenBSD. - #5007: Do not assume the "TERM" environment variable is always set. - #4606: Output a break before a list only if there was an empty line. - #5001: metas not cleaned properly in clenv_refine_in. - #2336: incorrect glob data for module symbols (bug #2336). - #4832: Remove extraneous dot in error message. - Anomaly in printing a unification error message. - #4947: Options which take string arguments are not backwards compatible. - #4156: micromega cache files are now hidden files. - #4871: interrupting par:abstract kills coqtop. - #5043: [Admitted] lemmas pick up section variables. - Fix name of internal refine ("simple refine"). - #5062: probably a typo in Strict Proofs mode. - #5065: Anomaly: Not a proof by induction. - Restore native compiler optimizations, they were disabled since 8.5! - #5077: failure on typing a fixpoint with evars in its type. - Fix recursive notation bug. - #5095: non relevant too strict test in let-in abstraction. - Ensuring that the evar name is preserved by "rename". - #4887: confusion between using and with in documentation of firstorder. - Bug in subst with let-ins. - #4762: eauto weaker than auto. - Remove if_then_else (was buggy). Use tryif instead. - #4970: confusion between special "{" and non special "{{" in notations. - #4529: primitive projections unfolding. - #4416: Incorrect "Error: Incorrect number of goals". - #4863: abstract in typeclass hint fails. - #5123: unshelve can impact typeclass resolution - Fix a collision about the meta-variable ".." in recursive notations. - Fix printing of info_auto. - #3209: Not_found due to an occur-check cycle. - #5097: status of evars refined by "clear" in ltac: closed wrt evars. - #5150: Missing dependency of the test-suite subsystems in prerequisite. - Fix a bug in error printing of unif constraints - #3941: Do not stop propagation of signals when Coq is busy. - #4822: Incorrect assertion in cbn. - #3479 parsing of "{" and "}" when a keyword starts with "{" or "}". - #5127: Memory corruption with the VM. - #5102: bullets parsing broken by calls to parse_entry. Various documentation improvements Changes from V8.5pl1 to V8.5pl2 =============================== Critical bugfix - Checksums of .vo files dependencies were not correctly checked. - Unicode-to-ASCII translation was not injective, leading in a soundness bug in the native compiler. Other bugfixes - #4097: more efficient occur-check in presence of primitive projections - #4398: type_scope used consistently in "match goal". - #4450: eauto does not work with polymorphic lemmas - #4677: fix alpha-conversion in notations needing eta-expansion. - Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. - #4644: a regression in unification. - #4725: Function (Error: Conversion test raised an anomaly) and Program (Error: Cannot infer this placeholder of type) - #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings - #4752: CoqIDE crash on files not ended by ".v". - #4777: printing inefficiency with implicit arguments - #4818: "Admitted" fails due to undefined universe anomaly after calling "destruct" - #4823: remote counter: avoid thread race on sockets - #4841: -verbose flag changed semantics in 8.5, is much harder to use - #4851: [nsatz] cannot handle duplicated hypotheses - #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant of nsatz - #4880: [nsatz_compute] generates invalid certificates if given redundant hypotheses - #4881: synchronizing "Declare Implicit Tactic" with backtrack. - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. triggered by CoqIDE - #4069, #4718: congruence fails when universes are involved. Universes - Disallow silently dropping universe instances applied to variables (forward compatible) - Allow explicit universe instances on notations, when they can apply to the head reference of their expansion. Build infrastructure - New update on how to find camlp5 binary and library at configure time. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.25 2016/07/02 10:17:18 jaapb Exp $ d3 4 a6 4 SHA1 (coq-8.6.tar.gz) = 617a6f86d09dde0e409f3fa22268daf7be3f5bba RMD160 (coq-8.6.tar.gz) = 3d5e539c40732620e65f28988b118d2e0d663aa5 SHA512 (coq-8.6.tar.gz) = 9f5f4913fda8cf83683fec9398b42d4567207c3d4b52b4638d5e09a24ed25a43905fb57a9fac1bb9f9d681bd47f3560e1da74e79348b3a3fd93e2e8c686cebae Size (coq-8.6.tar.gz) = 5538848 bytes @ 1.25 log @Updated package to latest version, 8.5pl1. Also fixed a packaging bug that had buildlink paths show up in the Coq_config module, and added a patch from upstream to allow compilation with 4.03. Changes: Critical bugfix - The subterm relation for the guard condition was incorrectly defined on primitive projections (#4588) Plugin development tools - add a .merlin target to the makefile Various performance improvements (time, space used by .vo files) Other bugfixes - Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v - Added compatibility coercions from Specif.v which were present in Coq 8.4. - Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic. - Allow to unset the refinement mode of Instance in ML - Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite. - Add -compat 8.4 econstructor tactics, and tests - Add compatibility Nonrecursive Elimination Schemes - Fixing the "No applicable tactic" non informative error message regression on apply. - Univs: fix get_current_context (bug #4603, part I) - Fix a bug in Program coercion code - Fix handling of arity of definitional classes. - #4630: Some tactics are 20x slower in 8.5 than 8.4. - #4627: records with no declared arity can be template polymorphic. - #4623: set tactic too weak with universes (regression) - Fix incorrect behavior of CS resolution - #4591: Uncaught exception in directory browsing. - CoqIDE is more resilient to initialization errors. - #4614: "Fully check the document" is uninterruptable. - Try eta-expansion of records only on non-recursive ones - Fix bug when a sort is ascribed to a Record - Primitive projections: protect kernel from erroneous definitions. - Fixed bug #4533 with previous Keyed Unification commit - Win: kill unreliable hence do not waitpid after kill -9 (Close #4369) - Fix strategy of Keyed Unification - #4608: Anomaly "output_value: abstract value (outside heap)". - #4607: do not read native code files if native compiler was disabled. - #4105: poor escaping in the protocol between CoqIDE and coqtop. - #4596: [rewrite] broke in the past few weeks. - #4533 (partial): respect declared global transparency of projections in unification.ml - #4544: Backtrack on using full betaiota reduction during keyed unification. - #4540: CoqIDE bottom progress bar does not update. - Fix regression from 8.4 in reflexivity - #4580: [Set Refine Instance Mode] also used for Program Instance. - #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683. - STM: Print/Extraction have to be skipped if -quick - #4542: CoqIDE: STOP button also stops workers - STM: classify some variants of Instance as regular `Fork nodes. - #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity"). - Do not give a name to anonymous evars anymore. See bug #4547. - STM: always stock in vio files the first node (state) of a proof - STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530 - Don't fail fatally if PATH is not set. - #4537: Coq 8.5 is slower in typeclass resolution. - #4522: Incorrect "Warning..." on windows. - #4373: coqdep does not know about .vio files. - #3826: "Incompatible module types" is uninformative. - #4495: Failed assertion in metasyntax.ml. - #4511: evar tactic can create non-typed evars. - #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported. - #4519: oops, global shadowed local universe level bindings. - #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed. - #4548: Coqide crashes when going back one command @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.24 2016/02/06 16:08:36 jaapb Exp $ d3 6 a8 7 SHA1 (coq-8.5pl1.tar.gz) = 92722ffc2be6948e0074b211bb556ad4b911ebd6 RMD160 (coq-8.5pl1.tar.gz) = 04c540ab1033fd6b0e4c121b73ed56557708e7a5 SHA512 (coq-8.5pl1.tar.gz) = c9a5bba1abc3b2216cb43595230387751277412988b44af1555ffccdc109a9eef69422867e0062d92dfc73ffcbbe24f53ff583224c28cae3f9bda1ae21dd547b Size (coq-8.5pl1.tar.gz) = 5366774 bytes SHA1 (patch-Makefile.build) = 1b711ef9490a07c9d02b5a8ca9a38c252e322b4f SHA1 (patch-Makefile.common) = f53dd334d3e14a0e0c3ef91bac9a6c1745cbb591 SHA1 (patch-configure.ml) = 6e2f44091216348a12131592bf29f0f7fd93a4fe @ 1.24 log @Updated package to latest version, 8.5. The changeset is over 500 lines long, so I will not include it here, but details can be found in the CHANGES file in the source. (the previous version was V8.4.) @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.23 2015/12/29 06:22:54 dholland Exp $ d3 4 a6 4 SHA1 (coq-8.5.tar.gz) = 0a0d124b1869d7e20cfcf3f71f086488c146f883 RMD160 (coq-8.5.tar.gz) = 551d35ac96436d98112fa1a17bcc075ee307c627 SHA512 (coq-8.5.tar.gz) = 28835a9dc4c926f97b14d23fe746e45e17942003e29807ec59f301eb0b697d704f05afc4cccd31b83bc27e9877d079d00e94a2101ba16ae32f4134e90ad011fb Size (coq-8.5.tar.gz) = 5346653 bytes d8 1 a8 1 SHA1 (patch-Makefile.common) = 67131e197d25a087d845dfa6fa93729f0b2eaa00 @ 1.23 log @pkglint @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.22 2015/11/03 22:50:33 agc Exp $ d3 7 a9 5 SHA1 (coq-8.4pl6.tar.gz) = c89525295659a805661ef91da24ecfb94e226953 RMD160 (coq-8.4pl6.tar.gz) = f57f6e5732d3977f3346dda2749f4b9628604018 SHA512 (coq-8.4pl6.tar.gz) = 238bc6e28348f40f5619aa28d2e871179d9edeb6eb3f2521af6f407e24a889c8c68fa11c8b12e026f016f0fb7d5006447c3ab7eeae0804fc082d65774aefe0ef Size (coq-8.4pl6.tar.gz) = 4099815 bytes SHA1 (patch-Makefile.build) = e4d8b329bc085855b38035c62a63fbb2f3895234 @ 1.22 log @Add SHA512 digests for distfiles for lang category Problems found with existing digests: Package nhc98 distfile nhc98src-1.22.tar.gz a8adc8f22371998ee0657bc0e01058a57d876abc [recorded] 81975fcb5f1dda5efeaabc30ce8c6dceae55e591 [calculated] Problems found locating distfiles: Package gcc-aux: missing distfile ada-bootstrap.i386.dragonfly.36A.tar.bz2 Package gcc-aux: missing distfile ada-bootstrap.i386.freebsd.84.tar.bz2 Package gcc-aux: missing distfile ada-bootstrap.x86_64.dragonfly.36A.tar.bz2 Package gcc-aux: missing distfile ada-bootstrap.x86_64.freebsd.84.tar.bz2 Package gcc-aux: missing distfile ada-bootstrap.x86_64.solaris.511.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.i386.dragonfly.36A.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.i386.freebsd.84.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.x86_64.dragonfly.36A.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.x86_64.freebsd.84.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.x86_64.solaris.511.tar.bz2 Package ghc7: missing distfile ghc-7.6.3-boot-i386-unknown-freebsd.tar.xz Package icc11: missing distfile l_cproc_p_11.1.080.tgz Package jini: missing distfile jini-1_2_1_001-src.zip Package oo2c: missing distfile oo2c_32-2.0.11.tar.bz2 Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-freebsd-10-amd64-20150301.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-5-i386-20150301.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-6-i386-20150301.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-7-earmv6hf-20150306.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-7-sparc64-20150301.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk7u60-bin-dragonfly-3.8-amd64-20140719.tar.bz2 Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-freebsd-10-amd64-20150301.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-5-i386-20150301.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-6-i386-20150301.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-7-earmv6hf-20150306.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-7-sparc64-20150301.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk7u60-bin-dragonfly-3.8-amd64-20140719.tar.bz2 Package oracle-jdk8: missing distfile jdk-8u60-linux-i586.tar.gz Package oracle-jdk8: missing distfile jdk-8u60-solaris-x64.tar.gz Package oracle-jre8: missing distfile jre-8u60-linux-i586.tar.gz Package oracle-jre8: missing distfile jre-8u60-solaris-x64.tar.gz Package sun-jdk6: missing distfile jdk-6u45-linux-i586.bin Package sun-jdk6: missing distfile jdk-6u45-solaris-i586.sh Package sun-jdk7: missing distfile jdk-7u72-linux-i586.tar.gz Package sun-jdk7: missing distfile jdk-7u72-solaris-i586.tar.gz Package sun-jre6: missing distfile jce_policy-6.zip Package sun-jre6: missing distfile jre-6u45-linux-x64.bin Package sun-jre6: missing distfile jre-6u45-solaris-x64.sh Package sun-jre7: missing distfile jre-7u72-linux-i586.tar.gz Package sun-jre7: missing distfile jre-7u72-solaris-i586.tar.gz Otherwise, existing SHA1 digests verified and found to be the same on the machine holding the existing distfiles (morden). All existing SHA1 digests retained for now as an audit trail. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.21 2015/04/25 13:41:18 jaapb Exp $ d7 1 a7 1 SHA1 (patch-Makefile.build) = 3fa72d701a80f363ef637e3cbd0e4c2d410da6c4 @ 1.21 log @Updated coq to version 8.4pl6. Changes from previous version include (apart from bugfixes): - Coq compilation made possible with forthcoming ocaml 4.03. - command for locating exists notation in refman changed. - Various improvements of the Reference Manual (especially its html version) - implicit arguments of local definitions fixed (possible source of incompatibilities). - New command "Print Debug GC". - Function cannot define graph. - Optimizing compilation of pattern matching. - Better inference of impossible cases in pattern-matching. - Evar leak in pattern-matching compilation - ill-typed replacement in "change ... with ...". - unbound evars in "change ... with ...". - wrong return clause of a match pattern in Ltac. - cleared local hints for autounfold. - cleared local hints for autounfold. - lost evars in "change ... with ...". - supporting let-ins in constructors for vm_compute - unfortunate typo in compare_height. - unfortunate typos in absorption lemmas over bool. - Full support of utf8 Greek letters (block U0370) in coqdoc @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.20 2014/10/09 22:19:01 jaapb Exp $ d5 1 @ 1.20 log @Revbump because of ocaml 4.02, added compilation patch (already in repository upstream) and updated package to use ocaml.mk framework. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.19 2014/05/13 14:52:28 jaapb Exp $ d3 3 a5 3 SHA1 (coq-8.4pl4.tar.gz) = 4dfc3a1ae65f5c480ddc4387d21549a526183e00 RMD160 (coq-8.4pl4.tar.gz) = 19e3fe905f5db09710b1f862f21e9b57c28f9704 Size (coq-8.4pl4.tar.gz) = 4067355 bytes a6 1 SHA1 (patch-kernel_univ.ml) = 2208e539870d6793b807bae46e0955b5f814f3fc @ 1.19 log @Update of package to version 8.4pl4. Changes include: Changes from V8.4pl3 to V8.4pl4 =============================== WARNING: The current logic of Coq is now known to be inconsistent with Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B. For more details, see: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm2.v;hb=HEAD or https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm3.v;hb=HEAD Kernel - Unsound check of elimination sort. - Fix guard condition for nested cofixpoints. - Univ constraints of module subtyping were not propagated. Tactics - A new option "Set Stable Omega" ensures that repeated identical calls to omega will produce identical proof terms. This option is off by default for maximal compatibility, but should be pretty safe to activate. - The interpretation of the open_constr tactic argument was erroneously firing type classes resolution in some corner cases. This has been fixed. The tactic argument type open_constr_wTC is provided for retro compatibility purposes. - Fixing bug (fixing precedence of ltac variables over variables in env) introduces rare and justified tactic failure. Bug fixes - micromega: solved an ambiguous symbol resolution. - Coq always uses / as separator between directories on all platforms. - remove trailing '\r' from file names returned by coqtop. - bug correction in proving inversion principles for Function. - ocamlbuild: minor fixes related to camlp4 and cross-compilation. Changes from V8.4pl2 to V8.4pl3 =============================== Ide_slave XML interface - 20120712, 20130419 : Invalidated protocol versions - From 20130419 extra datastructure : union (Inl "" = , Inr _ = ...) - 20130419~1 : new toplevel entry : message, not send by coptop v8.4 and not handle by coqide v8.4. A message has a level and a content (of string). Message levels are Debug of string, Info, Notice, Warning and Error. - 20130425 : * new toplevel entry : feedback, once again not send by coqtop v8.4 and not handle by coqide v8.4. A feedback gives the id of the sentence it provides info about and a content. Feedback contents are Processed, AddedAxiom and GlobRef of Util.loc * string * string * string * string * must provide an attribute id of type int. It is OK in coqtop v8.4 to alwais send Bug fixes - Fixing a significant efficiency leak in the code of the field tactic. - Fix caching of local hint database in typeclasses eauto which could miss some hypotheses. - Fix automatic solving of obligation in program, which was not trying to solve obligations that had no undefined dependencies left. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.18 2013/10/27 22:22:31 joerg Exp $ d7 1 @ 1.18 log @Don't use -fno-defer-pop. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.17 2013/10/26 19:44:33 asau Exp $ d3 3 a5 3 SHA1 (coq-8.4pl2.tar.gz) = adcef430b8e27663e8ea075e646112f7d4d51fa6 RMD160 (coq-8.4pl2.tar.gz) = 4860eaff4c8f0a235d3fcf162199eaa5fe1db2da Size (coq-8.4pl2.tar.gz) = 4145112 bytes a6 1 SHA1 (patch-configure) = 1ad232e16d397a762e61c000d1859c70d2447fc1 @ 1.17 log @Accept GNU Make 4 and later. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.16 2013/04/20 08:21:49 jaapb Exp $ d7 1 a7 1 SHA1 (patch-configure) = e1addbbc2ac9117e086dbe51f2e0c314d9f8ca93 @ 1.16 log @Updated package to the latest version, 8.4pl2. Changes include: Bug fixes - Solved bugs : #2466 #2629 #2668 #2750 #2839 #2869 #2954 #2955 #2959 #2962 #2966 #2967 #2969 #2970 #2975 #2976 #2977 #2978 #2981 #2983 #2995 #3000 #3004 #3008 - Partially fixed bugs : #2830 #2949 - Coqtop should now react more reliably when receiving interrupt signals: all the "try...with" constructs have been protected against undue handling of the Sys.Break exception. Coqide - The Windows-specific code handling the interrupt button of Coqide had to be reworked (cf. bug #2869). Now, in Win32 this button does not target a specific coqtop client, but instead sends a Ctrl-C to any process sharing its console with Coqide. To avoid awkward effects, it is recommended to launch Coqide via its icon, its menu, or in a dedicated console window. Extraction - The option Extraction AccessOpaque is now set by default, restoring compatibility of older versions of Coq (cf bug #2952). @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.15 2013/01/22 15:32:03 jaapb Exp $ d7 1 @ 1.15 log @Updated lang/coq to the newest version, 8.4pl1. Changes include: 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. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.14 2012/10/29 11:33:17 jaapb Exp $ d3 3 a5 3 SHA1 (coq-8.4pl1.tar.gz) = 23d403dbe9e410a99c584d0210dc527950051679 RMD160 (coq-8.4pl1.tar.gz) = fa472852de474ed5b83ddd4bd5a303f32b5dba94 Size (coq-8.4pl1.tar.gz) = 4139808 bytes @ 1.14 log @Taken over maintainership (as discussed with previous maintainer, richards@@cs.princeton.edu). Updated package to use PLIST_VARS and CONF_FILES. Updated coq to version 8.4. Changes include: Logic - Standard eta-conversion now supported (dependent product only). - Guard condition improvement: subterm property is propagated through beta-redex blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x"; this allows for instance to use "rewrite ... in ..." without breaking the guard condition. Vernacular commands - The "Reset" command is now supported again in files given to coqc or Load. - "Show Script" now indents again the displayed scripts. It can also work correctly across Load'ed files if the option "Unset Atomic Load" is used. - "Open Scope" can now be given the delimiter (e.g. Z) instead of the full scope name (e.g. Z_scope). - Commands "Back" and "BackTo" are now handling the proof states. They may perform some extra steps of backtrack to avoid states where the proof state is unavailable (typically a closed proof). - The commands "Suspend" and "Resume" have been removed. - A basic Show Script has been reintroduced (no indentation). - New command "Set Parsing Explicit" for deactivating parsing (and printing) of implicit arguments (useful for teaching). - New command "Grab Existential Variables" to transform the unresolved evars at the end of a proof into goals. - It is now mandatory to have a space (or tabulation or newline or end-of-file) after a "." ending a sentence. - In SearchAbout, the [ ] delimiters are now optional. - New command "Add/Remove Search Blacklist ...": a Search or SearchAbout or similar query will never mention lemmas whose qualified names contain any of the declared substrings. The default blacklisted substrings are "_admitted" "_subproof" "Private_". - When the output file of "Print Universes" ends in ".dot" or ".gv", the universe graph is printed in the DOT language, and can be processed by Graphviz tools. - New command "Print Sorted Universes". - The undocumented and obsolete option "Set/Unset Boxed Definitions" has been removed, as well as syntaxes like "Boxed Fixpoint foo". - A new option "Set Default Timeout n / Unset Default Timeout". - Qed now uses information from the reduction tactics used in proof script to avoid conversion at Qed time to go into a very long computation. - New command "Show Goal ident" to display the statement of a goal, even a closed one (available from Proof General). - Command "Proof" accept a new modifier "using" to force generalization over a given list of section variables at section ending. - New command "Arguments" generalizing "Implicit Arguments" and "Arguments Scope" and that also allows to rename the parameters of a definition and to tune the behavior of the tactic "simpl". Specification language and Notations - Most compatibility notations of the standard library are now tagged as (compat xyz), where xyz is a former Coq version, for instance "8.3". These notations behave as (only parsing) notations, except that they may triggers warnings (or errors) when used while Coq is not in a corresponding -compat mode. - To activate these compatibility warnings, use "Set Verbose Compat Notations" or the command-line flag -verbose-compat-notations. - For a strict mode without these compatibility notations, use "Unset Compat Notations" or the command-line flag -no-compat-notations. - Maximal implicit arguments can now be set locally by { }. The registration traverses fixpoints and lambdas. Because there is conversion in types, maximal implicit arguments are not taken into account in partial applications (use eta expanded form with explicit { } instead). - Added support for recursive notations with binders (allows for instance to write "exists x y z, P"). - Structure/Record printing can be disable by "Unset Printing Records". In addition, it can be controlled on type by type basis using "Add Printing Record" or "Add Printing Constructor". - Pattern-matching compilation algorithm: in "match x, y with ... end", possible dependencies of x (or of the indices of its type) in the type of y are now taken into account. Tactics - An annotation "eqn:H" or "eqn:?" can be added to a "destruct" or "induction" to make it generate equations in the spirit of "case_eq". The former syntax "_eqn" is discontinued. - The name of the hypothesis introduced by tactic "remember" can be set via the new syntax "remember t as x eqn:H" (wish #2489). - Still no general "info" tactical, but new specific tactics info_auto, info_eauto, info_trivial which provides information on the proofs found by auto/eauto/trivial. Display of these details could also be activated by "Set Info Auto"/"Set Info Eauto"/"Set Info Trivial". - Details on everything tried by auto/eauto/trivial during a proof search could be obtained by "debug auto", "debug eauto", "debug trivial" or by a global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial". - New command "r string" in Ltac debugger that interprets "idtac string" in Ltac code as a breakpoint and jumps to its next use. - Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy) have been removed, since Why2 has not been maintained for the last few years. The Why3 plugin should be a suitable replacement in most cases. - New proof engine. - Scripts can now be structured thanks to bullets - * + and to subgoal delimitation via { }. Note: for use with Proof General, a cvs version of Proof General no older than mid-July 2011 is currently required. - Support for tactical "info" is suspended. - Support for command "Show Script" is suspended. - New tactics constr_eq, is_evar and has_evar for use in Ltac. - Removed the two-argument variant of "decide equality". - New experimental tactical "timeout ". Since is a time in second for the moment, this feature should rather be avoided in scripts meant to be machine-independent. - Fix in "destruct": removal of unexpected local definitions in context might result in some rare incompatibilities (solvable by adapting name hypotheses). - Introduction pattern "_" made more robust. - Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C. - Unification in "apply" supports unification of patterns of the form ?f x y = g(x,y) (compatibility ensured by using "Unset Tactic Pattern Unification"). It also supports (full) betaiota. - Tactic autorewrite does no longer instantiate pre-existing existential variables (theoretical source of possible incompatibilities). - Tactic "dependent rewrite" now supports equality in "sig". - Tactic omega now understands Zpred (wish #1912) and can prove any goal from a context containing an arithmetical contradiction (wish #2236). - Using "auto with nocore" disables the use of the "core" database (wish #2188). This pseudo-database "nocore" can also be used with trivial and eauto. - Tactics "set", "destruct" and "induction" accepts incomplete terms and use the goal to complete the pattern assuming it is non ambiguous. - When used on arguments with a dependent type, tactics such as "destruct", "induction", "case", "elim", etc. now try to abstract automatically the dependencies over the arguments of the types (based on initial ideas from Chung-Kil Hur, extension to nested dependencies suggested by Dan Grayson) - Tactic "injection" now failing on an equality showing no constructors while it was formerly generalizing again the goal over the given equality. - In Ltac, the "context [...]" syntax has now a variant "appcontext [...]" allowing to match partial applications in larger applications. - When applying destruct or inversion on a fixpoint hiding an inductive type, recursive calls to the fixpoint now remain folded by default (rare source of incompatibility generally solvable by adding a call to simpl). - In an ltac pattern containing a "match", a final "| _ => _" branch could be used now instead of enumerating all remaining constructors. Moreover, the pattern "match _ with _ => _ end" now allows to match any "match". A "in" annotation can also be added to restrict to a precise inductive type. - The behavior of "simpl" can be tuned using the "Arguments" vernacular. In particular constants can be marked so that they are always/never unfolded by "simpl", or unfolded only when a set of arguments evaluates to a constructor. Last one can mark a constant so that it is unfolded only if the simplified term does not expose a match in head position. Libraries - Reals: changed definition of PI, no more axiom about sin(PI/2). - SetoidPermutation: a notion of permutation for lists modulo a setoid equality. - BigN: fixed the ocaml code doing the parsing/printing of big numbers. - MSetRBT: a new implementation of MSets via Red-Black trees (initial contribution by Andrew Appel). - MSetAVL: for maximal sharing with the new MSetRBT, the argument order of Node has changed (this should be transparent to regular MSets users). - Extension of the abstract part of Numbers, which now provide axiomatizations and results about many more integer functions, such as pow, gcd, lcm, sqrt, log2 and bitwise functions. These functions are implemented for nat, N, BigN, Z, BigZ. See in particular file NPeano for new functions about nat. - The definition of types positive, N, Z is now in file BinNums.v - Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains an internal module Z implementing the Numbers interface for integers. This module Z regroups: * all functions over type Z : Z.add, Z.mul, ... * the minimal proofs of specifications for these functions : Z.add_0_l, ... * an instantation of all derived properties proved generically in Numbers : Z.add_comm, Z.add_assoc, ... A large part of ZArith is now simply compatibility notations, for instance Zplus_comm is an alias for Z.add_comm. The direct use of module Z is now recommended instead of relying on these compatibility notations. - Similar major reorganization of NArith, via a module N in NArith/BinNat.v - Concerning the positive datatype, BinPos.v is now in a specific directory PArith, and contains an internal submodule Pos. We regroup there functions such as Pos.add Pos.mul etc as well as many results about them. These results are here proved directly (no Number interface for strictly positive numbers). - Note that in spite of the compatibility layers, all these reorganizations may induce some marginal incompatibilies in scripts. In particular: * the "?=" notation for positive now refers to a binary function Pos.compare, instead of the infamous ternary Pcompare (now Pos.compare_cont). * some hypothesis names generated by the system may changed (typically for a "destruct Z_le_gt_dec") since naming is done after the short name of the head predicate (here now "le" in module Z instead of "Zle", etc). * the internals of Z.add has changed, now relying of Z.pos_sub. - Also note these new notations: * "= XP SP1. - The communication between CoqIDE and Coqtop is now done via a dialect of XML. - The backtrack engine of CoqIDE has been reworked, it now uses the "Backtrack" command similarly to Proof General. - The Coqide parsing of sentences has be reworked and now supports tactic delimitation via { }. - Coqide now accepts the Abort command (wish #2357). - Coqide can read coq_makefile files as "project file" and use it to set automatically options to send to coqtop. - Preference files have moved to $XDG_CONFIG_HOME/coq and accelerators are not stored as a list anymore. Internal infrastructure - Opaque proofs are now loaded lazily by default. This allows to be almost as fast as -dont-load-proofs, while being safer (no creation of axioms) and avoiding feature restrictions (Print and Print Assumptions work ok). - Revised hash-consing code allowing more sharing of memory - Experimental support added for camlp4 (the one provided alongside ocaml), simply pass option -usecamlp4 to ./configure. By default camlp5 is used. - Revised build system: no more stages in Makefile thanks to some recursive aspect of recent gnu make, use of vo.itarget files containing .v to compile for both make and ocamlbuild, etc. - Support of cross-compilation via mingw from unix toward Windows, contact P. Letouzey for more informations. - New Makefile rules mli-doc to make html of mli in dev/doc/html and full-stdlib to get a (huge) pdf reflecting the whole standard library. Extraction - By default, opaque terms are now truly considered opaque by extraction: instead of accessing their body, they are now considered as axioms. The previous behaviour can be reactivated via the option "Set Extraction AccessOpaque". - The pretty-printer for Haskell now produces layout-independant code - A new command "Separate Extraction cst1 cst2 ..." that mixes a minimal extracted environment a la "Recursive Extraction" and the production of several files (one per coq source) a la "Extraction Library". - New option "Set/Unset Extraction KeepSingleton" for preventing the extraction to optimize singleton container types. - The extraction now identifies and properly rejects a particular case of universe polymorphism it cannot handle yet (the pair (I,I) being Prop). - Support of anonymous fields in record (#2555). Tools - Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq, $XDG_DATA_DIRS/coq, and user-contribs before the standard library. - Coq rc file has moved to $XDG_CONFIG_HOME/coq. - Major changes to coq_makefile: * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work; * mlihtml generates doc of mli, install-doc install the html doc in DOCDIR with the same policy as vo in COQLIB; * More variables are given by coqtop -config, others are defined only if the users doesn't have defined them elsewhere. Consequently, generated makefile should work directly on any architecture; * Packagers can take advantage of $(DSTROOT) introduction. Installation can be made in $XDG_DATA_HOME/coq; * -arg option allows to send option as argument to coqc. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.13 2011/03/28 20:39:26 tonio Exp $ d3 3 a5 3 SHA1 (coq-8.4.tar.gz) = 2987aa418dd96a0df7284afe296293cb28814ef5 RMD160 (coq-8.4.tar.gz) = 6824f9542c823c7d943a59acefb90ff9c9dbe37a Size (coq-8.4.tar.gz) = 4134779 bytes a6 2 SHA1 (patch-ide_preferences.ml) = 625b8e7fe7b4f1612c7f43bd634070aff928fdfb SHA1 (patch-ide_utils_okey.ml) = d61ad0e2ea23c531bb4f5e9540f8581a72b54da8 @ 1.13 log @Update lang/coq to 8.3pl1 Changes from V8.3 to V8.3pl1 o Type inference, notations and implicit arguments bug fixes - #2448 (alpha-renaming problems with notations internally using binders) - #2454 (pattern-matching sometimes not supporting type casts) - fixing combined use of non-implicit and explictly-declared implicit arguments in inductive arities - restored support for using some ident with different scopes in notations o Ltac and tactics bug fixes - #2414 (rewrite in not looking for eq_ind in the right module) - #2433 (new "is_evar"/"has_evar" to restore support for matching evars in Ltac) - #2453 (dependent destruction) - loop in dependent destruction - new "constr_eq" tactic for restoring support for term equality test in Ltac - setoid rewrite under cases and abstraction fixed o Coqdoc and documentation bugs - #2418 (wrong URLs in documentation) - #2441 (coqdoc bug in Mergesort.v) - #2445 (correct support for "'" character in coqdoc links to notations) - fixed wrong use of "moduleid" instead of "module" in coqdoc html indexes - fixing parsing of Multiplication and Division signs (unicode 0xD7 and 0xF7) o Compilation - #2432 (support for compilation with camlp5 6.02.0) - support for compilation with ocaml >= 3.09.3 restored o Extraction - #2413 (prevent type-unsafe optimisations of pattern matching) - Identifiers of a development aimed to be extracted should avoid containing "__", since the extraction make various use of this sub-string, leading to potential name clashes. This was already so in V8.3, but not announced, as mentionned by #2421. o Miscellaneous bug fixes - #2412 (anomaly Ploc.Exc when using Ltac Debug) - #2419 (redundant opp_compare removed) - #2427 (Module Functor claims Signature does not match) - #2431 (compliance of CoqIDE use of mutexes with FreeBSD) - #2434 (anomaly DuringSyntaxChecking with Local/Global prefixes) - a few improvements in efficiency @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.12 2010/11/14 20:53:02 tonio Exp $ d3 6 a8 4 SHA1 (coq-8.3pl1.tar.gz) = 3fae9fa2fd6f39c9fb3c0b67fcd5e71f1e7a5f9f RMD160 (coq-8.3pl1.tar.gz) = 687983bcaca723299b6ea902a1e1b07338209d55 Size (coq-8.3pl1.tar.gz) = 3756961 bytes SHA1 (patch-ac) = 59516eb44aa6cedb4f897b5ac3e8fe0aa69aba0f @ 1.12 log @Update lang/coq to 8.3 Main changes: Includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that extends ring to systems of polynomial equations) and a few new libraries (a certification of mergesort, a new library of finite sets with computational and logical contents separated). This version also comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. Here is an excerpt: * new operator <+ for conveniently chaining application of functors * new round of extension of the modular library of arithmetic * support for matching terms with binders in Ltac, * linking notations in coqdoc, * quote tactic now working on arbitrary expressions, * Lemma and co accept parameters that are automatically introduced, * interactive proofs in module types, * a beautifying coqc option for pretty-printing files See the file CHANGES for a full log of changes. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.11 2010/11/07 15:39:55 tonio Exp $ d3 3 a5 5 SHA1 (coq-8.3.tar.gz) = 6c6472b6a41429e78d979eacd8ff58bd6f6c9da4 RMD160 (coq-8.3.tar.gz) = 9e42266001c0a22b39662be86960a05e454fc2fb Size (coq-8.3.tar.gz) = 3736420 bytes SHA1 (patch-aa) = 851efa1859b4d8dc7bad549792a5966b549f868e SHA1 (patch-ab) = f20f78c936e18ca195933375f37fc5b816827604 @ 1.11 log @Make it build with newer gmake @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.10 2009/12/12 21:12:43 asau Exp $ d3 6 a8 7 SHA1 (coq-8.2pl1.tar.gz) = 4aed3302adc2edbaa5d97984512c1c13014bd649 RMD160 (coq-8.2pl1.tar.gz) = dd5758a94bb3de49967cec76baa33eb5169659ce Size (coq-8.2pl1.tar.gz) = 3600620 bytes SHA1 (patch-aa) = 2725d9fb667f6a66bf9cb6dd0bdcdbd94d8c1fd6 SHA1 (patch-ab) = 207d8138baf9bfbb78d816c24dcc367869a60569 SHA1 (patch-ac) = 30780c9f96ad16c814a5edc50bd1edbd030aa9b5 SHA1 (patch-ad) = 9bb28ca4eeb77d53d3665fbc4575bea1f57c738c @ 1.10 log @Support staged installation. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.9 2009/09/05 20:44:58 tonio Exp $ d7 1 a7 1 SHA1 (patch-ab) = 6573a11efab6ef7c026e8fd39b23e8596dee5a61 @ 1.9 log @Update lang/coq to 8.2pl1 Changes from V8.1 to V8.2 ========================= Language - If a fixpoint is not written with an explicit { struct ... }, then all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. - New experimental typeclass system giving ad-hoc polymorphism and overloading based on dependent records and implicit arguments. - New syntax "let 'pat := b in c" for let-binding using irrefutable patterns. - New syntax "forall {A}, T" for specifying maximally inserted implicit arguments in terms. - Sort of Record/Structure, Inductive and CoInductive defaults to Type if omitted. - Support for optional "where" notation clauses for record fields. - (Co)Inductive types can be defined as records (e.g. "CoInductive stream := { hd : nat; tl : stream }.") - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent statements. - Support for sort-polymorphism on constants denoting inductive types. - Several evolutions of the module system (handling of module aliases, functorial module types, an Include feature, etc). - Prop now a subtype of Set (predicative and impredicative forms). - Recursive inductive types in Prop with a single constructor of which all arguments are in Prop is now considered to be a singleton type. It consequently supports all eliminations to Prop, Set and Type. As a consequence, Acc_rect has now a more direct proof [possible source of easily fixed incompatibility in case of manual definition of a recursor in a recursive singleton inductive type]. - New syntax to do implicit generalization in binders and inside terms. - New tentative syntax for introduction of record objects without mentioning the constructor {| field := body; ... |}, turning missing fields into holes (compatible with refine and Program). Vernacular commands - Added option Global to "Arguments Scope" for section surviving. - Added option "Unset Elimination Schemes" to deactivate the automatic generation of elimination schemes. - Modification of the Scheme command so you can ask for the name to be automatically computed (e.g. Scheme Induction for nat Sort Set). - New command "Combined Scheme" to build combined mutual induction principles from existing mutual induction principles. - New command "Scheme Equality" to build a decidable (boolean) equality for simple inductive datatypes and a decision property over this equality (e.g. Scheme Equality for nat). - Added option "Set Equality Scheme" to make automatic the declaration of the boolean equality when possible. - Source of universe inconsistencies now printed when option "Set Printing Universes" is activated. - New option "Set Printing Existential Instances" for making the display of existential variable instances explicit. - Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the "compute"/"cbv" reduction strategy, respectively meaning reduce only, or everything but, the constants id1 ... idn. "lazy" alone or followed by "[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply all of beta-iota-zeta-delta, possibly restricting delta. - New command "Strategy" to control the expansion of constants during conversion tests. It generalizes commands Opaque and Transparent by introducing a range of levels. Lower levels are assigned to constants that should be expanded first. - New options Global and Local to Opaque and Transparent. - New command "Print Assumptions" to display all variables, parameters or axioms a theorem or definition relies on. - "Add Rec LoadPath" now provides references to libraries using partially qualified names (this holds also for coqtop/coqc option -R). - SearchAbout supports negated search criteria, reference to logical objects by their notation, and more generally search of subterms. - "Declare ML Module" now allows to import .cmxs files when Coq is compiled in native code with a version of OCaml that supports native Dynlink (>= 3.11). - New command "Create HintDb name [discriminated]" to explicitely declare a new hint database and optionaly turn on a discrimination net implementation to index all the lemmas in the database. - New commands "Hint Transparent" and "Hint Opaque" to set the unfolding status of definitions used by auto. This information is taken into account by the discrimination net and the unification algorithm. - "Hint Extern" now takes an optional pattern and applies the given tactic all the time if no pattern is given. - Specific sort constraints on Record now taken into account. - "Print LoadPath" supports a path argument to filter the display. Libraries - Several parts of the libraries are now in Type, in particular FSets, SetoidList, ListSet, Sorting, Zmisc. This may induce a few incompatibilities. In case of trouble while fixing existing development, it may help to simply declare Set as an alias for Type (see file SetIsType). - New arithmetical library in theories/Numbers. It contains: * an abstract modular development of natural and integer arithmetics in Numbers/Natural/Abstract and Numbers/Integer/Abstract * an implementation of efficient computational bounded and unbounded integers that can be mapped to processor native arithmetics. See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN for unbounded natural numbers and Numbers/Integer/BigZ for unbounded integers. * some proofs that both older libraries Arith, ZArith and NArith and newer BigN and BigZ implement the abstract modular development. This allows in particular BigN and BigZ to already come with a large database of basic lemmas and some generic tactics (ring), This library has still an experimental status, as well as the processor-acceleration mechanism, but both its abstract and its concrete parts are already quite usable and could challenge the use of nat, N and Z in actual developments. Moreover, an extension of this framework to rational numbers is ongoing, and an efficient Q structure is already provided (see Numbers/Rational/BigQ), but this part is currently incomplete (no abstract layer and generic lemmas). - Many changes in FSets/FMaps. In practice, compatibility with earlier version should be fairly good, but some adaptations may be required. * Interfaces of unordered ("weak") and ordered sets have been factorized thanks to new features of Coq modules (in particular Include), see FSetInterface. Same for maps. Hints in these interfaces have been reworked (they are now placed in a "set" database). * To allow full subtyping between weak and ordered sets, a field "eq_dec" has been added to OrderedType. The old version of OrderedType is now called MiniOrderedType and functor MOT_to_OT allow to convert to the new version. The interfaces and implementations of sets now contain also such a "eq_dec" field. * FSetDecide, contributed by Aaron Bohannon, contains a decision procedure allowing to solve basic set-related goals (for instance, is a point in a particular set ?). See FSetProperties for examples. * Functors of properties have been improved, especially the ones about maps, that now propose some induction principles. Some properties of fold need less hypothesis. * More uniformity in implementations of sets and maps: they all use implicit arguments, and no longer export unnecessary scopes (see bug #1347) * Internal parts of the implementations based on AVL have evolved a lot. The main files FSetAVL and FMapAVL are now much more lightweight now. In particular, minor changes in some functions has allowed to fully separate the proofs of operational correctness from the proofs of well-balancing: well-balancing is critical for efficiency, but not anymore for proving that these trees implement our interfaces, hence we have moved these proofs into appendix files FSetFullAVL and FMapFullAVL. Moreover, a few functions like union and compare have been modified in order to be structural yet efficient. The appendix files also contains alternative versions of these few functions, much closer to the initial Ocaml code and written via the Function framework. - Library IntMap, subsumed by FSets/FMaps, has been removed from Coq Standard Library and moved into a user contribution Cachan/IntMap - 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, ...) (exceptional source of incompatibilities). - Boolean operators moved from module Bool to module Datatypes (may need to rename qualified references in script and force notations || and && to be at levels 50 and 40 respectively). - The constructors xI and xO of type positive now have postfix notations "~1" and "~0", allowing to write numbers in binary form easily, for instance 6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v). - Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular a better power function). - Changes in ZArith: several additional lemmas (used in theories/Numbers), especially in Zdiv, Znumtheory, Zpower. Moreover, many results in Zdiv have been generalized: the divisor may simply be non-null instead of strictly positive (see lemmas with name ending by "_full"). An alternative file ZOdiv proposes a different behavior (the one of Ocaml) when dividing by negative numbers. - Changes in Arith: EqNat and Wf_nat now exported from Arith, some constructions on nat that were outside Arith are now in (e.g. iter_nat). - In SetoidList, eqlistA now expresses that two lists have similar elements at the same position, while the predicate previously called eqlistA is now equivlistA (this one only states that the lists contain the same elements, nothing more). - Changes in Reals: * Most statement in "sigT" (including the completeness axiom) are now in "sig" (in case of incompatibility, use proj1_sig instead of projT1, sig instead of sigT, etc). * More uniform naming scheme (identifiers in French moved to English, consistent use of 0 -- zero -- instead of O -- letter O --, etc). * Lemma on prod_f_SO is now on prod_f_R0. * Useless hypothesis of ln_exists1 dropped. * New Rlogic.v states a few logical properties about R axioms. * RIneq.v extended and made cleaner. - Slight restructuration of the Logic library regarding choice and classical logic. Addition of files providing intuitionistic axiomatizations of descriptions: Epsilon.v, Description.v and IndefiniteDescription.v. - Definition of pred and minus made compatible with the structural decreasing criterion for use in fixpoints. - Files Relations/Rstar.v and Relations/Newman.v moved out to the user contribution repository (contribution CoC_History). New lemmas about transitive closure added and some bound variables renamed (exceptional risk of incompatibilities). Notations, coercions, implicit arguments and type inference - More automation in the inference of the return clause of dependent pattern-matching problems. - Experimental allowance for omission of the clauses easily detectable as impossible in pattern-matching problems. - Improved inference of implicit arguments, now working inside record declarations. - New options "Set Maximal Implicit Insertion", "Set Reversible Pattern Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit Defensive" for controlling inference and use of implicit arguments. - New modifier in "Implicit Arguments" to force an implicit argument to be maximally inserted. - New options Global and Local to "Implicit Arguments" for section surviving or non export outside module. - Level "constr" moved from 9 to 8. - Structure/Record now printed as Record (unless option Printing All is set). - Support for parametric notations defining constants. - Insertion of coercions below product types refrains to unfold constants (possible source of incompatibility). - New support for fix/cofix in notations. Tactic Language - Second-order pattern-matching now working in Ltac "match" clauses (syntax for second-order unification variable is "@@?X"). - Support for matching on let bindings in match context using syntax "H := body" or "H := body : type". - (?X ?Y) patterns now match any application instead of only unary applications (possible source of incompatibility). - Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer). - The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]" is extended so that at most one expr_i may have the form "expr .." or just "..". Also, n can be different from the number of subgoals generated by expr_0. In this case, the value of expr (or idtac in case of just "..") is applied to the intermediate subgoals to make the number of tactics equal to the number of subgoals. - A name used as the name of the parameter of a lemma (like f in "apply f_equal with (f:=t)") is now interpreted as a ltac variable if such a variable exists (this is a possible source of incompatibility and it can be fixed by renaming the variables of a ltac function into names that do not clash with the lemmas parameter names used in the tactic). - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression. - "let rec ... in ... " now supported for expressions without explicit parameters; interpretation is lazy to the contrary of "let ... in ..."; hence, the "rec" keyword can be used to turn the argument of a "let ... in ..." into a lazy one. - Patterns for hypotheses types in "match goal" are now interpreted in type_scope. - A bound variable whose name is not used elsewhere now serves as metavariable in "match" and it gets instantiated by an identifier (allow e.g. to extract the name of a statement like "exists x, P x"). - New printing of Ltac call trace for better debugging. - The C-zar (formerly know as declarative) proof language is now properly documented. Tactics - New tactics "apply -> term", "apply <- term", "apply -> term in ident", "apply <- term in ident" for applying equivalences (iff). - "apply" and "rewrite" now take open terms (terms with undefined existentials) as input. - Slight improvement of the hnf and simpl tactics when applied on expressions with explicit occurrences of match or fix. - New tactics "eapply in", "erewrite", "erewrite in". - New tactics "ediscriminate", "einjection", "esimplify_eq". - Tactics "discriminate", "injection", "simplify_eq" now support any term as argument. Clause "with" is also supported. - Unfoldable references can be given by notation's string rather than by name in unfold. - The "with" arguments are now typed using informations from the current goal: allows support for coercions and more inference of implicit arguments. - Application of "f_equal"-style lemmas works better. - Tactics elim, case, destruct and induction now support variants eelim, ecase, edestruct and einduction. - Tactics destruct and induction now support the "with" option and the "in" clause option. If the option "in" is used, an equality is added to remember the term to which the induction or case analysis applied (possible source of parsing incompatibilities when destruct or induction is part of a let-in expression in Ltac; extra parentheses are then required). - New support for "as" clause in tactics "apply in" and "eapply in". - Some new intro patterns: * intro pattern "?A" genererates a fresh name based on A. Caveat about a slight loss of compatibility: Some intro patterns don't need space between them. In particular intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it is still legal but equivalent to intros ?a ?b. * intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))" for right-associative constructs like /\ or exists. - Several syntax extensions concerning "rewrite": * "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites occur only on the first subgoal: in particular, side-conditions of the "rewrite A" are not concerned by the "rewrite B,C". * "rewrite A by tac" allows to apply tac on all side-conditions generated by the "rewrite A". * "rewrite A at n" allows to select occurrences to rewrite: rewrite only happen at the n-th exact occurrence of the first successful matching of A in the goal. * "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A". * "rewrite !A" means rewriting A as long as possible (and at least once). * "rewrite 3?A" means rewriting A at most three times. * "rewrite ?A" means rewriting A as long as possible (possibly never). * many of the above extensions can be combined with each other. - Introduction patterns better respect the structure of context in presence of missing or extra names in nested disjunction-conjunction patterns [possible source of rare incompatibilities]. - New syntax "rename a into b, c into d" for "rename a into b; rename c into d" - New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]" to do induction-inversion on instantiated inductive families ? la BasicElim. - Tactics "apply" and "apply in" now able to reason modulo unfolding of constants (possible source of incompatibility in situations where apply may fail, e.g. as argument of a try or a repeat and in a ltac function); versions that do not unfold are renamed into "simple apply" and "simple apply in" (usable for compatibility or for automation). - Tactics "apply" and "apply in" now able to traverse conjunctions and to select the first matching lemma among the components of the conjunction; tactic "apply" also able to apply lemmas of conclusion an empty type. - Tactic "apply" now supports application of several lemmas in a row. - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)". - New tactic "instantiate" (without argument). - Tactic firstorder "with" and "using" options have their meaning swapped for consistency with auto/eauto (source of incompatibility). - Tactic "generalize" now supports "at" options to specify occurrences and "as" options to name the quantified hypotheses. - New tactic "specialize H with a" or "specialize (H a)" allows to transform in-place a universally-quantified hypothesis (H : forall x, T x) into its instantiated form (H : T a). Nota: "specialize" was in fact there in earlier versions of Coq, but was undocumented, and had a slightly different behavior. - New tactic "contradict H" can be used to solve any kind of goal as long as the user can provide afterwards a proof of the negation of the hypothesis H. If H is already a negation, say ~T, then a proof of T is asked. If the current goal is a negation, say ~U, then U is saved in H afterwards, hence this new tactic "contradict" extends earlier tactic "swap", which is now obsolete. - Tactics f_equal is now done in ML instead of Ltac: it now works on any equality of functions, regardless of the arity of the function. - New options "before id", "at top", "at bottom" for tactics "move"/"intro". - Some more debug of reflexive omega (romega), and internal clarifications. Moreover, romega now has a variant "romega with *" that can be also used on non-Z goals (nat, N, positive) via a call to a translation tactic named zify (its purpose is to Z-ify your goal...). This zify may also be used independantly of romega. - Tactic "remember" now supports an "in" clause to remember only selected occurrences of a term. - Tactic "pose proof" supports name overwriting in case of specialization of an hypothesis. - Semi-decision tactic "jp" for first-order intuitionistic logic moved to user contributions (subsumed by "firstorder"). Program - Moved useful tactics in theories/Program and documented them. - Add Program.Basics which contains standard definitions for functional programming (id, apply, flip...) - More robust obligation handling, dependent pattern-matching and well-founded definitions. - Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer which argument decreases structurally. - Program Lemma, Axiom etc... now permit to have obligations in the statement iff they can be automatically solved by the default tactic. - Renamed "Obligations Tactic" command to "Obligation Tactic". - New command "Preterm [ of id ]" to see the actual term fed to Coq for debugging purposes. - New option "Transparent Obligations" to control the declaration of obligations as transparent or opaque. All obligations are now transparent by default, otherwise the system declares them opaque if possible. - Changed the notations "left" and "right" to "in_left" and "in_right" to hide the proofs in standard disjunctions, to avoid breaking existing scripts when importing Program. Also, put them in program_scope. Type Classes - New "Class", "Instance" and "Program Instance" commands to define classes and instances documented in the reference manual. - New binding construct "`{Class_1 param_1 .. param_n, Class_2 ...}" for binding type classes, usable everywhere. - New command " Print Classes " and " Print Instances some_class " to print tables for typeclasses. - New default eauto hint database "typeclass_instances" used by the default typeclass instance search tactic. - New theories directory "theories/Classes" for standard typeclasses declarations. Module Classes.RelationClasses is a typeclass port of Relation_Definitions plus a generic development of algebra on n-ary heterogeneous predicates. Setoid rewriting - Complete (and still experimental) rewrite of the tactic based on typeclasses. The old interface and semantics are almost entirely respected, except: - Import Setoid is now mandatory to be able to call setoid_replace and declare morphisms. - "-->", "++>" and "==>" are now right associative notations declared at level 55 in scope signature_scope. Their introduction may break existing scripts that defined them as notations with different levels. - One can use [Typeclasses Opaque/Transparent [cst]] to indicate that [cst] should not be unfolded during unification for morphism resolution, by default all constants are transparent. - The [setoid_rewrite]'s semantics change when rewriting with a lemma: it can rewrite two different instantiations of the lemma at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics. [setoid_rewrite] will also try to rewrite under binders now, and can succeed on different terms than before. In particular, it will unify under let-bound variables. When called through [rewrite], the semantics are unchanged though. - [Add Morphism term : id] has different semantics when used with parametric morphism: it will try to find a relation on the parameters too. The behavior has also changed with respect to default relations: the most recently declared Setoid/Relation will be used, the documentation explains how to customize this behavior. - Parametric Relation and Morphism are declared differently, using the new [Add Parametric] commands, documented in the manual. - Setoid_Theory is now an alias to Equivalence, scripts building objects of type Setoid_Theory need to unfold (or [red]) the definitions of Reflexive, Symmetric and Transitive in order to get the same goals as before. Scripts which introduced variables explicitely will not break. - The order of subgoals when doing [setoid_rewrite] with side-conditions is now always the same: first the new goal, then the conditions. - New standard library modules Classes.Morphisms declares standard morphisms on refl/sym/trans relations. Classes.Morphisms_Prop declares morphisms on propositional connectives and Classes.Morphisms_Relations on generalized predicate connectives. Classes.Equivalence declares notations and tactics related to equivalences and Classes.SetoidTactics defines the setoid_replace tactics and some support for the "Add *" interface, notably the tactic applied automatically before each "Add Morphism" proof. - User-defined subrelations are supported, as well as higher-order morphisms and rewriting under binders. The tactic is also extensible entirely in Ltac. The documentation has been updated to cover these features. - [setoid_rewrite] and [rewrite] now support the [at] modifier to select occurrences to rewrite, and both use the [setoid_rewrite] code, even when rewriting with leibniz equality if occurrences are specified. Extraction - Improved behavior of the Caml extraction of modules: name clashes should not happen anymore. - The command Extract Inductive has now a syntax for infix notations. This allows in particular to map Coq lists and pairs onto Caml ones: Extract Inductive list => list [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. - In pattern matchings, a default pattern "| _ -> ..." is now used whenever possible if several branches are identical. For instance, functions corresponding to decidability of equalities are now linear instead of quadratic. - A new instruction Extraction Blacklist id1 .. idn allows to prevent filename conflits with existing code, for instance when extracting module List to Ocaml. CoqIDE - CoqIDE font defaults to monospace so as indentation to be meaningful. - CoqIDE supports nested goals and any other kind of declaration in the middle of a proof. - Undoing non-tactic commands in CoqIDE works faster. - New CoqIDE menu for activating display of various implicit informations. - Added the possibility to choose the location of tabs in coqide: (in Edit->Preferences->Misc) - New Open and Save As dialogs in CoqIDE which filter *.v files. Tools - New stand-alone .vo files verifier "coqchk". - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir". - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R. - The binary "parser" has been renamed to "coq-parser". coqdoc - Improved coqdoc and dump of globalization information to give more meta-information on identifiers. All categories of Coq definitions are supported, which makes typesetting trivial in the generated documentation. - A "--interpolate" option permits to use typesetting information from the typechecked part of the file to typeset identifiers appearing in Coq escapings inside the documentation. - Better handling of utf8 ("--utf8" option) and respect of spaces in the source. - Support for hyperlinking and indexing developments in the TeX output. - New option "color" of the coqdoc style file to render identifiers using colors. - Additional macros in the TeX ouput allowing to customize indentation and size of empty lines. New environment "coqdoccode" for Coq code. Miscellaneous - Coq installation provides enough files so that Ocaml's extensions need not the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5). - New commands "Set Whelp Server" and "Set Whelp Getter" to customize the Whelp search tool. - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into "Test Printing Let for ref" and "Test Printing If for ref". - An overhauled build system (new Makefiles); see dev/doc/build-system.txt. - Add -browser option to configure script. - Build a shared library for the C part of Coq, and use it by default on non-(Windows or MacOS) systems. Bytecode executables are now pure. The behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and -custom configure options. - Complexity tests can be skipped by setting the environment variable COQTEST_SKIPCOMPLEXITY. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.8 2008/01/12 11:48:40 tonio Exp $ d9 1 @ 1.8 log @Update lang/coq to 8.1pl3 hanges from V8.1pl2 to V8.1pl3 =============================== Bug fixes - A critical bug and a few other bugs have been fixed. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.7 2007/12/01 13:05:36 tonio Exp $ d3 6 a8 5 SHA1 (coq-8.1pl3.tar.gz) = c06141891c2a793ff6b4bc1f106d9477b3a9a52e RMD160 (coq-8.1pl3.tar.gz) = f8f4749e1014cb47a83915550713cf9ce1992e34 Size (coq-8.1pl3.tar.gz) = 3003593 bytes SHA1 (patch-aa) = bdfe2986da84b13c7df383caf969858707be83f3 SHA1 (patch-ab) = b252096b0bef5fee0a2f719ddc17021fd013ed64 @ 1.7 log @Update lang/coq to 8.2pl2 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. @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.6 2007/02/25 15:03:52 tonio Exp $ d3 4 a6 4 SHA1 (coq-8.1pl2.tar.gz) = 33ab31abffe42559a5c8341b66a0520805337526 RMD160 (coq-8.1pl2.tar.gz) = e45451fdd41b1f979febcfb2c0dbd19a39d09256 Size (coq-8.1pl2.tar.gz) = 2997185 bytes SHA1 (patch-aa) = 4a518e52aea4a2e239754b6a8123b9a2fdaefa00 @ 1.6 log @Update lang/coq to 8.1 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). @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.5 2006/01/27 19:22:58 tonio Exp $ d3 5 a7 4 SHA1 (coq-8.1.tar.gz) = 151aca5b7c919eeb39ba3c6fecec836b7953b206 RMD160 (coq-8.1.tar.gz) = 548d2e25e7813567252f9b176f318619a780d729 Size (coq-8.1.tar.gz) = 2977142 bytes SHA1 (patch-aa) = 4cc1fdee8074aaa3d1af24151c2d2277522ec9bc @ 1.5 log @Update lang/coq to 8.0pl3 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... @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.4 2006/01/16 14:34:34 tonio Exp $ d3 4 a6 4 SHA1 (coq-8.0pl3.tar.gz) = b182f25b8e6591139281f7078d049aaa7f0408d8 RMD160 (coq-8.0pl3.tar.gz) = 925a65fdd0c96f4fe6082bc7bfb8483c83b5fea7 Size (coq-8.0pl3.tar.gz) = 2309002 bytes SHA1 (patch-aa) = 2ef8be34bd9c77229ef9a2a6e5d04891d7e159da @ 1.4 log @Make lang/coq compile with ocaml 3.09 by applying the patch distributed by the coq team Bump PKGREVISION, and require ocaml >= 3.09 @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.3 2005/02/24 09:03:06 agc Exp $ d3 4 a6 4 SHA1 (coq-8.0pl2.tar.gz) = 58d0c054c9b50ef12b462f97df2424ee3baa25ab RMD160 (coq-8.0pl2.tar.gz) = ead90ff5957ccc9cbcd0f3769b75a7fb440b383b Size (coq-8.0pl2.tar.gz) = 2285855 bytes SHA1 (patch-aa) = 1e2592d494be250de76debfb79687611d4b7b870 @ 1.3 log @Add RMD160 digests @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.2 2005/02/05 11:19:02 adrianp Exp $ d6 1 a6 1 SHA1 (patch-aa) = e62e14729a2dacd7e6e9aa4418c911b34cc4aee5 @ 1.2 log @- Update of coq from 7.4 to 8.0pl2 - Initial patches supplied by Antoine Reilles, thanks ! - Lots of changes/fixes/updates, see: CHANGES @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.1.1.1 2003/03/22 20:21:17 kristerw Exp $ d4 1 @ 1.1 log @Initial revision @ text @d1 1 a1 1 $NetBSD: distinfo,v 1.1.1.1 2003/03/22 18:20:55 kristerw Exp $ d3 3 a5 3 SHA1 (coq-7.4.tar.gz) = 82fe0094cde8a766e3ba0a77c731b4ef2345a41b Size (coq-7.4.tar.gz) = 1537547 bytes SHA1 (patch-aa) = ce59dda44ac5f81834f9f60a7f87524c90f6cb6e @ 1.1.1.1 log @By popular demand, move coq-7.4 from math to lang in order to be consistent 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. @ text @@