- 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

• Files Changed
• Browse Source

- Update to version 8.12.2.

• Files Changed
• Browse Source