• Files Changed
• Browse Source

- Update to version 8.12.2.

• Files Changed
• Browse Source

- Update to version 8.12.1. This contains mostly bug fixes:
  * Polymorphic side-effects inside monomorphic definitions were
    incorrectly handled as not inlined. This allowed deriving an
    inconsistency.
  * Regression in error reporting after SSReflect's case tactic.
    A generic error message "Could not fill dependent hole in
    apply" was reported for any error following case or elim.
  * Several bugs with Search.
  * The details environment introduced in coqdoc in Coq 8.12 can
    now be used as advertised in the reference manual.
  * View menu "Display parentheses" introduced in CoqIDE in
    Coq 8.12 now works correctly.
- Use memoryperjob constraint instead of %limit_build macro.

• Files Changed
• Browse Source

- Update to version 8.12.0.
  * 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. 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.

• Files Changed
• Browse Source

- Update to version 8.11.2.
  * Fixed a kernel issue where using Require inside a section
    caused an anomaly when closing the section.
  * Fixed normalization in conclusion of custom induction scheme.
  * Fixed a loss of location of some tactic errors.
  * Ignore -native-compiler option when built without native
    compute support.
  * Fixed a segfault issue with CoqIDE completion.
  * Highlighting style is now consistently applied to all three
    buffers of CoqIDE.

• Files Changed
• Browse Source

- Update to version 8.11.1, with upstream support for OCaml 4.10.
  * Allow more inductive types in Unset Positivity Checking mode.
  * Fixed bugs in dealing with precedence of notations in custom
    entries.
  * In primitive floats, print a warning when parsing a decimal
    value that is not exactly a binary64 floating-point number.
    For instance, parsing 0.1 will print a warning whereas parsing
    0.5 won't.
  * Fixed an issue in CoqIDE about compiling file paths containing
    spaces.
  * Fixed an issue where Extraction Implicit on the constructor of
    a record was leading to an anomaly.
- Remove now obsolete ocaml-410-build.patch.

• Files Changed
• Browse Source

- The num library is required for OCaml 4.06 or later.
- Add ocaml-410-build.patch: fix build with OCaml 4.10.

• Files Changed
• Browse Source

- Update to version 8.11.0.
  * 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.
  * Many other cleanups and improvements have been performed and
    are further described in the changelog.
  * Special note on compatibility: Fixed bugs of Export and Import
    that can have a significant impact on user developments.
- Drop unneeded empty *.vos files.
- Update to version 8.10.2.
  * Fixed a critical bug of template polymorphism and nonlinear
    universes;
  * Fixed a few anomalies;
  * Fixed an 8.10 regression related to the printing of coercions
    associated to notations;
  * Fixed uneven dimensions of CoqIDE panels when window has been
    resized;
  * Fixed queries in CoqIDE.
- Update to version 8.10.0.
  * some quality-of-life bug fixes;
  * a critical bug fix related to template polymorphism;
  * native 63-bit machine integers;
  * a new sort of definitionally proof-irrelevant propositions: 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.
- Update to version 8.10.1.
  * Fix proof of False when using SProp
  * Fix an anomaly when unsolved evar in Add Ring
  * Fix Ltac regression in binding free names in uconstr
  * Fix handling of unicode input before space
  * Fix custom extraction of inductives to JSON
- Update version requirements.

• Files Changed
• Browse Source

- Initial release based on version 8.9.1.

• Browse Source