* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=65
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=63
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=60
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=52
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=50
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=48
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=44
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=42
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=40
* 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).
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=38
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=37
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=36
- Update to version 8.13.0.
* 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.
* 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.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=22
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=19
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=17
* 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.
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=15
- 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.
OBS-URL: https://build.opensuse.org/request/show/774600
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=9
