1.8.0

• allow Coq 8.17, drop 8.14
• allow Mathcomp 1.16, drop 1.13-14
• add mathcomp-algebra dependency
• add Prop-level theory for All and Has
• rename AllPn->allPnIn, HasPn->hasPnIn
• add trans_eq, if_triv, theory for foldl/r and onth in prelude, rename prefixP -> prefixE
• expand seq theory in seqext, including "big cat" lemmas
• refactor slice theory, split interval theory on unique sequences into useqord, uslice and uconsec

1.7.0

• remove Program switches in options
• switch namespace to pcm to disambiguate with FCSL proper
• split out theory of filter/last/index and binary relations to seqext
• add a theory of finding the last element by predicate
• generalize intervals to arbitrary eqType
• generalize sepit_perm and sepitF lemmas to Prop-level predicates
• add umpreim_cond, umpreimPt, rangeF & umfilt_predC to unionmap

1.6.0

• allow Coq 8.16
• added a theory of non-symmetric separating relations
• refactored the theory of sub-PCMs and local relations
• added a theory of map prefixes for unionmaps
• added boolean reflection and rcons/last lemmas to prelude, \In lemmas to pred
• refactored automated lemma infrastructure
• extracted sequence intervals into a separate sub-theory
• added several natmap theories required by current FCSL examples (will be deprecated and removed in future releases): continuous & complete maps, leq surgery, exec & growth

1.5.1

Updated minimal required version of Coq to 8.14

1.5.0

• added automation for general PCMs (currently contains a single pullX automation)
• factored out common automation infrastructure for PCMs and maps
• added finite PCM products
• added a PCM instance for option
• major refactoring of the natmap theory
• additions to prelude and the unionmap theory, speed up andP reflections

1.4.0

Update minimal required versions of the dependencies: Coq 8.13 and Mathcomp 1.12

• added behd (remove the head/minimal key+value) function for finmap
• added a class for omap-like functions on unionmaps
• expanded theory for working with natmaps as histories
• code updated according to the new requirements of dependencies: #[export] attributes, lemma renamings etc
• removed problematic setoid for funext
• removed deprecated subPCM construction

1.3.0

Minimum required versions of the dependencies: Coq 8.11 and Mathcomp 1.10

• Refactor unionmap class
• Add PCM morphisms and separation relations
• Various additions and fixes

1.1.1

• Add support for Mathcomp 1.10 and drop support for the previous version
• Extend the range of supported Coq versions: 8.7 .. 8.11

1.2.0

• Upgrade minimum required versions of the dependencies to Coq 8.10 and Mathcomp 1.10
• Simplify some proofs
• Various maintenance fixes: warnings, opam file tweaks

1.1.0

• Extend supported Coq and Mathcomp versions (check opam info coq-fcsl-pcm.1.1.0 for the current supported versions)
• ordtype module: add reflexivity lemma for oleq
• heap module : rename path_last into path_last_nat to avoid name clashes with ordtype's path_last
• Rename Make into_CoqProject to make it more uniform across Coq projects
• Switch to opam 2.0 file format
• Various maintenance fixes: warnings, typos, etc.