Chapar 8.17.0 maintenance release

Maintenance release compatible with Coq 8.14 to 8.19, with the following changes:

Fixed

• Build with Coq 8.19 and beyond

Chapar 8.16.0 maintenance release

Maintenance release compatible with Coq 8.14 to 8.18, with the following changes:

Changed

• Adjust build for Coq 8.18 and beyond
• Use Dune wrapping for OCaml modules
• Remove boilerplate for OCamlbuild
• Move bash scripts to scripts directory
• Use standard theories/src directory names

Fixed

• Stores build with Dune 3.6 or later
• Nix CI configuration
• List lemma deprecations in 8.18

Chapar 8.15.0 maintenance release

Maintenance release compatible with Coq 8.14 to 8.17, featuring the following changes:

Changed

• Removed unecessary imports
• Adjust build for Coq 8.16 and beyond

Fixed

• Deprecations related to Stdlib Nat module

Chapar 8.14.0 maintenance release

Maintenance release compatible with Coq 8.14 and 8.15, featuring the following changes:

Changed

• Add hint locality everywhere and consequently require Coq 8.14 or later

Fixed

• Use consistent conventions for Require Import

Chapar 8.13.0 maintenance release

Maintenance release compatible with Coq 8.13, featuring the following changes:

Changed

• Make most hints local
• Adjust build for Coq 8.13 and beyond

Chapar 8.12.0 maintenance release

Maintenance release compatible with Coq 8.10 to 8.12, featuring the following changes:

Changed

• OCaml OPAM package definition uses Dune
• Reorganize extraction to support Dune
• Coq OPAM package definition uses Dune
• Declare all scopes and consequently require Coq 8.10 or later

Added

• Support for OCaml builds with Dune
• Support for Coq builds with Dune

Fixed

• Remove dependency on a local functional extensionality axiom

Removed

• All uses of UTF-8

Chapar 8.11.0 maintenance release

Maintenance release with Coq 8.11 compatibility, featuring the following changes:

Fixed

• Compatibility with Coq 8.11
• Ignore more untracked files such as .vos
• Remove mention of extracted OPAM package in README.md

Changed

• Add Proof using annotations for faster .vos/.vio compilation
• Ignore undeclared scope warning

Chapar 8.10.0 maintenance release

Maintenance release with Coq 8.9 and 8.10 compatibility, featuring the following changes:

Removed

• Unused library lemmas and functions originally from a formalization of separation logic that were vendored

Fixed

• Hint and declaration deprecation warnings
• Switch from deprecated omega tactic to lia

Changed

• Use LF newlines everywhere, in place of CRLF

Chapar 8.9.0 maintenance release

Maintenance release after move to Coq-community, with Coq 8.9 compatibility, featuring the following changes:

• port from Coq 8.4
• better organization of code into subdirectories
• extracted code builds with modern OCaml (>= 4.05.0) and Batteries (>= 2.8.0)
• modernize the build scripts to use coq_makefile features