- Update to version 8.20.0. The most impactful changes are:
  * A mechanism to add user-defined rewrite rules to Coq's reduction
    mechanisms; see chapter "User-defined rewrite rules".
  * Support for primitive strings in terms.
  * Reduction of the bytecode segment size, which in turn means
    that `.vo` files might now be considerably smaller.
- Notable breaking changes:
  * Syntactic global references passed through the `using` clauses
    of `auto`-like tactics are now handled as plain references
    rather than interpreted terms. In particular, their typeclass
    arguments will not be inferred. In general, the previous
    behaviour can be emulated by replacing `auto using foo` with
    `pose proof foo; auto`.
  * Argument order for the Ltac2 combinators `List.fold_left2` and
    `List.fold_right2` changed to be the same as in OCaml.
  * Importing a module containing a mutable Ltac2 definition does
    not undo its mutations. Replace `Ltac2 mutable foo :=
    some_expr.` with `Ltac2 mutable foo := some_expr. Ltac2 Set foo
    := some_expr.` to recover the previous behaviour.
  * Some renaming in the standard library. Deprecations are
    provided for a smooth transition.
- For more details, see the change log in coq-doc.

• Files Changed
• Browse Source

- Update to version 8.19.2.
  * Fixed a regression from Coq 8.18 in the presence of a defined
    field in a primitive `Record`.
  * Fixed an issue where the printer was sometimes failing to use a
    prefix or infix custom notation whose right-hand side refers to
    a different custom entry.
  * Fixed `abstract` failure in the presence of admitted goals in
    the surrounding proof.
  * Fixed issues when using Ltac2 in VsCoq due to incorrect state
    handling of Ltac2 notations.
  * Fixed `Include` on a module containing a record declared with
    `Primitive Projections`.
  * Fixed an issue in `Fixpoint` with no arguments.
  * Position error/warning tooltips correctly when multibyte UTF-8
    characters are present.

• Files Changed
• Browse Source

- Update to version 8.19.1.
  * Fixed incorrect abstraction of sort variables for opaque
    constants leading to an inconsistency.
  * Fixed memory corruption with `vm_compute` (rare but more
    likely with OCaml 5.1).
  * "Found no matching notation to enable or disable" is now a
    warning instead of an error.
  * Fixed undeclared universe with multiple uses of `abstract`.
  * Fixed incorrect printing of constructor values with multiple
    arguments, and over-parenthesizing of constructor printing.
  * Fixed incorrect declared type for Ltac2.FMap.fold.

• Files Changed
• Browse Source

- Update to version 8.19.0. The most impactful changes:
  * Sort polymorphism makes it possible to share common constructs
    over `Type`, `Prop` and `SProp`.
  * The notation `term%_scope` to set a scope only temporarily (in
    addition to `term%scope` for opening a scope applying to all
    subterms).
  * `lazy`, `simpl`, `cbn` and `cbv` and the associated `Eval` and
    `eval` reductions learned to do head reduction when given flag
    `head`.
  * New Ltac2 APIs, improved Ltac2 `exact` and dynamic building of
    Ltac2 term patterns.
  * New performance evaluation facilities: `Instructions` to count
    CPU instructions used by a command and Profiling system to
    produce trace files.
  * New command `Attributes` to assign attributes such as
    `deprecated` to a library file.
- Notable breaking changes:
  * `replace` with `by tac` does not automatically attempt to solve
    the generated equality subgoal using the hypotheses. Use `by
    first [assumption | symmetry;assumption | tac]` if you need the
    previous behaviour.
  * Removed old deprecated files from the standard library. 
- Use %fdupes in the documentation package.

• Files Changed
• Browse Source

- Revert last change: this is now set in ocaml-rpm-macros.
- Increase stack size limit in QEMU user space builds. Here ulimit
  has no effect, so we add a wrapper around ocamlopt.opt to PATH
  that adds "-s ..." to the qemu-<arch> command line.

• Files Changed
• Browse Source

- Increase stack size limit to fix build on riscv64.

• Files Changed
• Browse Source

- Update to version 8.18.0.
  * The default locality of `Hint` and `Instance` commands was
    switched to `export`.
  * The universe unification algorithm can now delay the commitment
    to a sort (the algorithm used to pick `Type`). Thanks to this
    feature many `Prop` and `SProp` annotations can be now omitted.
  * Ltac2 supports array literals, maps and sets of primitive
    datatypes such as names (of constants, inductive types, etc)
    and fine-grained control over profiling.
  * The warning system offers new categories, enabling finer
    (de)activation of specific warnings. This should be
    particularly useful to handle deprecations.
  * Many new lemmas useful for teaching analysis with Coq are now
    part of the standard library about real numbers.
  * The `#[deprecated]` attribute can now be applied to definitions.

• Files Changed
• Browse Source

- Update to version 8.17.1.
  * Fixed incorrect paths emitted by coqdep in some cases for META
    files which prevented dune builds for plugins from working
    correctly.
  * Fixed shadowing of record fields in extraction to OCaml.
  * Fixed an impossible-to-turn-off debug message "backtracking and
    redoing byextend on ...".
  * Fixed a major memory regression affecting MathComp 2.
- Classify desktop entry under Science instead of Education.
- Add screenshot URL to AppStream metadata.

• Files Changed
• Browse Source

- Update to version 8.17.0.
  * Fixed a logical inconsistency due to `vm_compute` in presence
    of side-effects in the enviroment (e.g. using Back or Fail).
  * It is now possible to dynamically enable or disable notations.
  * Support multiple scopes in `Arguments` and `Bind Scope`.
  * The tactics chapter of the manual has many improvements in
    presentation and wording. The documented grammar is semi-
    automatically checked for consistency with the implementation.
  * Fixes to the `auto` and `eauto` tactics, to respect hint
    priorities and the documented use of simple apply. This is a
    potentially breaking change.
  * New Ltac2 APIs, deep pattern-matching with `as` clauses and
    handling of literals, support for record types and preterms.
  * Move from :> to :: syntax for declaring typeclass fields as
    instances, fixing a confusion with declaration of coercions.
  * Standard library improvements.

• Files Changed
• Browse Source

- Build with ocaml-rpm-macros to get proper Requires and Provides
  for coq-devel. This should prevent incompatibilities with other
  Ocaml libraries when building native objects against coq-devel.

• Files Changed
• Browse Source

- Update to version 8.16.1.
  * Fixed the conversion of `Prod` values in the native compiler.
  * Added `SProp` check for opaque names in conversion.
  * Pass the correct environment to compute η-expansion of
    cofixpoints in VM and native compilation.
  * Fixed an inconsistency with conversion of primitive arrays, and
    associated incomplete strong normalization of primitive arrays
    with `lazy`.
  * `Print Assumptions` treats opaque definitions with missing
    proofs (as found in .vos files, produced using -vos) as axioms
    instead of ignoring them.

• Files Changed
• Browse Source

- Update to version 8.16.0.
  * The guard checker (see `Guarded`) now ensures strong
    normalization under any reduction strategy.
  * Irrelevant terms (in the `SProp` sort) are now squashed to a
    dummy value during conversion, fixing a subject reduction 
    issue and making proof conversion faster.
  * Introduction of reversible coercions, which allow coercions 
    relying on meta-level resolution such as type-classes or 
    canonical structures. Also allow coercions that do not fullfill
    the uniform inheritance condition.
  * Generalized rewriting support for rewriting with `Type`-valued 
    relations and in `Type` contexts, using the
    `Classes.CMorphisms` library.
  * Added the boolean equality scheme command for decidable 
    inductive types.
  * Added a `Print Notation` command.
  * Incompatibilities in name generation for Program obligations,
    `eauto` treatment of tactic failure levels, use of `ident` in
    notations, parsing of module expressions.
  * Standard library reorganization and deprecations.
  * Improve the treatment of standard library numbers by
    `Extraction`.
- Coq requires ocamlfind at runtime now.

• Files Changed
• Browse Source

- Update to version 8.15.2.
  * Tactics `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 ::= ...`.
  * Fixed an uncaught exception `UnableToUnify` with
    bidirectionality hints.
  * Fixed multiple CoqIDE bugs.
  * Fixed an incorrect implementation of `SFClassify`, allowing for
    a proof of `False` since 8.11.0, due to Axioms present in
    `Float.Axioms`.
- Rename coq.desktop to fr.inria.coq.coqide.desktop as the
  documentation suggests, add an accompanying metainfo file.
- Declare documentation as noarch.

• Files Changed
• Browse Source

- Update to version 8.15.1.
  * Fixes an inconsistency when using module subtyping with
    inductive types.
  * Speeds up CoqIDE on large files.
  * Fixes a bug where `coqc -vok` was not creating a .vok file.
  * Fixes a regression in `cbn`.
  * Improves usability of schemes with `elim foo using scheme with
    (P0 := ...)` (the `P0` name was not accessible in 8.15.0).

• Files Changed
• Browse Source

- Update to version 8.15.0.
  * The `apply with` tactic no longer renames arguments unless
    the compatibility flag `Apply With Renaming` is set.
  * Improvements to the `auto` tactic family, fixing `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.
  * For more details, see refman/changes.html in coq-doc.

• Files Changed
• Browse Source

- Update to version 8.14.1.
  * Fixed 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.
  * Fixed missing registration of universe constraints in Module
    Type elaboration.
  * Made `abstract` more robust with respect to Ltac `constr`
    bindings containing existential variables.
  * Correct support of trailing `let` by tactic `specialize`.
  * Fixed an anomaly with `Extraction Conservative Types` when
    extracting pattern-matching on singleton types.
  * Regular error instead of an anomaly when calling `Separate
    Extraction` in a module.

• Files Changed
• Browse Source

- Update to version 8.14.0.
  * 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.
  * For more details, see refman/changes.html in coq-doc.

• Files Changed
• Browse Source

- Add documentation package based on github.com/coq/doc until we
  can build the documentation directly in OBS.

• Files Changed
• Browse Source

- Update to version 8.13.2.
  * Fix crash when using vm_compute on an irreducible PArray.set.
  * Fix crash when loading .vo files containing a vm_compute
    normalized primitive array.
  * Fix Ltac2.Array.init computational complexity.

• Files Changed
• Browse Source

- Update to version 8.13.1.
  * Fix arities of VM opcodes for some floating-point operations
    that could cause memory corruption.

• Files Changed
• Browse Source