baserev update by copy to link target

• 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

baserev update by copy to link target

• Files Changed
• Browse Source

- Cover stdlib with %fdupes.

• 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).
  * Tactics `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 (Linux only) 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

baserev update by copy to link target

• Files Changed
• Browse Source

- Do the right thing if qemu_user_space_build is defined as 0.

• Files Changed
• Browse Source

- 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

- Revert last change: this is now set in ocaml-rpm-macros.

• Files Changed
• Browse Source

baserev update by copy to link target

• Files Changed
• Browse Source

- Increase stack size limit to fix build on riscv64.

• Files Changed
• Browse Source

baserev update by copy to link target

• 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

baserev update by copy to link target

• 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

baserev update by copy to link target

• 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

baserev update by copy to link target

• 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

baserev update by copy to link target

• Files Changed
• Browse Source