CHANGES

-----------------------------------------------------------------------------
22-01-17: RELEASE OPAM 1.8.2 for Coq 8.15

-----------------------------------------------------------------------------
21-03-18: RELEASE OPAM 1.8.1 for Coq 8.13 (commit d1929ff)

-----------------------------------------------------------------------------
20-09-23: RELEASE OPAM 1.8.0 for Coq 8.12 (commit 67f71af)

-----------------------------------------------------------------------------
19-11-05: RELEASE OPAM 1.7.0 for Coq 8.10 (commit 08b5481)

-----------------------------------------------------------------------------
19-02-11: RELEASE OPAM 1.6.0 for Coq 8.9 (commit 328aa06)

-----------------------------------------------------------------------------
18-05-04: RELEASE OPAM 1.5.0 for Coq 8.8 (commit a810c5b)

-----------------------------------------------------------------------------
17-11-10: RELEASE OPAM 1.4.0 for Coq 8.7 (SVN revision 2434)

17-11-10: [Vadim Zaliva]
- port to Coq 8.7

-----------------------------------------------------------------------------
17-01-11: RELEASE OPAM 1.3.0 for Coq 8.6 (SVN revision 2432)

17-01-11: [Vadim Zaliva]
- port to Coq 8.6

16-04-29:
- moved ListForall into ListUtil
- replaced Implicit Arguments by Arguments

16-04-28: prefix Require's by From Coq or From CoLoR to avoid problems
  when installing CoLoR with other libraries

-----------------------------------------------------------------------------
16-01-26: RELEASE OPAM 1.2.0 for Coq 8.5 (SVN revision 2394)

16-01-26:
- moved to Coq 8.5

16-01-20:
- Util/Relation/Tarski: proof that the least fixpoint can be reached by transfinite induction; corresponding induction principle; fixpoint on a sig type

16-01-12:
- Util/Nat/BoundNat: added vector of bounded natural numbers

16-01-06:
- Util/FMap/FMapUtil: Make now takes an FMapInterface.S as argument;
  moved parts of LSimple into a Domain submodule taking an FSetInterface.S
  as argument

15-05-05:
- Term/Lambda/LEta: eta-reduction
- Term/Lambda: extended all termination results to eta-reduction

15-04-30:
- Util/FSet/FSetUtil: added replace
- Term/Lambda/LSubs,LAlpha:
  . generalized seq and saeq by introducing subs_rel
  . added subs_rel_mon_preorder and sub_rel_mon_preorder_aeq

15-03-27:
- Util/Logic/LogicUtil: added split_all tactic
- reduced compilation time by improving some scripts
  CoLoR without Coccinelle now compiles in:
  -j1: 17'53" instead of 22'16" (-21.0%)
  -j3: 7'16" instead of 9'21" (-21.5%)
  -j20: 4'43" instead of 6'28" (-26.9%)
  CoLoR with Coccinelle now compiles in:
  -j1: 22'18" instead of 27'00" (-17.4%)
  -j3: 8'48" instead of 10'47" (-18.6%)
  -j20: 5'27" instead of 6'45" (-18.5%)
- Util/Option/ExcUtil: renamed into OptUtil
- Util/Nat/NatLt: renamed into BoundNat
- Util/Pair/LexOrder: renamed into PairLex
- Util/List/LexicographicOrder: renamed into ListLex
- Util/Nat/NatLeast: renamed into LeastNat

15-03-19:
- replaced Add Relation/Morphism by Instance everywhere
- Util/Nat/BoundNat:
  . replaced bnat by N and nfirst_nats by L
  . renamed and moved everything into NatLt
- removed Emacs local variables in Coccinelle

15-03-15:
- Util/List/ListRepeatFree: renamed into ListNodup,
  make_repeat_free renamed into remdup, repeat_free renamed into nodup
- Util/Relation/RelExtras: moved things to RelUtil and ExcUtil

-----------------------------------------------------------------------------
15-03-10: RELEASE OPAM 1.1.0 for Coq 8.4 (SVN revision 2156)

15-03-10:
- Util/Set/Ramsey: classical infinite Ramsey theorem
- Util/Set/FinSet: new file defining finiteness and providing finiteness lemmas
- Util/Set/InfSet: new file defining infiniteness
  and providing infiniteness lemmas
- Util/List/ListUtil: added select, pos, new lemmas on remove,
  and renamed mk_nat_lts into L
- Util/List/ListRepeatFree: added new lemmas
- Util/Nat/NatUtil: added smallest natural satisfying some property,
  and renamed nat_lt into N
- Util/Set/SetUtil: added new definitions and lemmas
- Util/Nat/NatLt: new file gathering old and new results about natural numbers
  smaller than some fixed bound (type N and function L)

-----------------------------------------------------------------------------
15-02-04: RELEASE OPAM 1.0.0 for Coq 8.4 (SVN revision 2104)

14-12-29: [Strub]
- Util/Vector/VecUtil: Vcast defined by matching on the equality proof argument
  (like eq_rect) instead of on the vector argument

14-02-19:
- Util/Vector/VecOrd: Vreln moved into VecUtil
- Util/Vector/VecEq: moved into VecOrd

14-01-28:
- Term/Lambda/LAlphaAlt: added Gabbay and Pitts definition of alpha-equivalence

-----------------------------------------------------------------------------
13-12-03: NEW RELEASE (SVN revision 2023)

13-10-04:
- Term/Lambda/LAlphaAlt: definitions of alpha-equivalence by Church and
  Krivine, and proof that they are equivalent to the one of Curry and Feys

-----------------------------------------------------------------------------
13-09-20: NEW RELEASE (SVN revision 2003)

13-09-20:
- Term/lambda/LSystemT: definition and termination proof of Goedel System T
- Util/Relation/OrdDec replaced by Util/Relation/OrdUtil

-----------------------------------------------------------------------------
13-09-16: NEW RELEASE (SVN revision 1983)

13-09-13:
- Term/Lambda/LCompClos: computability closure and proof that its ensures
  termination of higher-order rewrite systems
- Term/Lambda/LCompRewrite: higher-order rewriting
  and its associated CP structure
- Term/Lambda/LCall: lexicographic ordering on partial function calls
- Term/Lambda/LCompInt: interpretation of positive inductive types
  as computability predicates

13-08-14:
- Term/Lambda and Util: various additions

13-08-02:
- Util/Relation/Tarski: Knaster-Tarski theorem

13-06-05:
- Term/Lambda: reorganized definitions so that Inductive's and various
functions including substitution are defined out of any module

12-11-06:
- Util/Relation/SN: added proof that SN -> ~NT following
  http://www.labri.fr/perso/casteran/CoqArt/gen-rec/SRC/not_decreasing.v
- removed IS_NotSN_FB subsumed by previous result
- moved IS_NotSN into NotSN_IS

-----------------------------------------------------------------------------
12-10-23: NEW RELEASE (SVN revision 1751)

12-10-23:
- Term/Lambda/LTerm: pure lambda-terms with names variables
- Term/Lambda/LSubs: higher-order simultaneous substitutions
- Term/Lambda/LAlpha: alpha-equivalence
- Term/Lambda/LBeta: beta-reduction
- Term/Lambda/LComp: axiomatic version of Tait-Girard computability
- Term/Lambda/LSimple: typing relation with simple types
- Term/Lambda/LCompSimpl: termination of beta-reduction on simply-typed terms

-----------------------------------------------------------------------------
12-08-22: NEW RELEASE (SVN revision 1743)

12-08-22:
- migration to Coq 8.4

11-03-25:
- Util/FGraph/TransClos: transitive closure of a finite graph
- Util/FGraph/FGraph: library on finite graphs

10-11-30: [Ould-Biha]
- Term/WithArity/AInfSeq: infinite sequences
- Term/WithArity/ASubterm: the subterm relation is finitely branching
- Util/Nat/NatLeast: min of a non-empty set of nats
- Term/WithArity/ADepRel: relation on defined symbols implied by rules

10-11-24:
- Util/List/ListUtil: sub_list
- Util/Vector/VecFilterPerm: vector filtering with permutations
- Filter/AFilterPerm: non-collapsing arguments filtering with permutations

10-11-16: [Koprowski]
- MatrixInt/ATropicalInt: tropical matrix interpretations

-----------------------------------------------------------------------------
10-10-28: NEW RELEASE (SVN revision 1341)

10-10-27:
- migration to Coq 8.3

10-06-30: [Stratulat]
- added Sorin Stratulat's patch to Coccinelle's RPO for allowing a
quasi-ordering on symbols instead of an ordering

-----------------------------------------------------------------------------
09-12-07: NEW RELEASE (SVN revision 1000)

09-11-04:
- DP/ADP: use Dershowitz improvement for defining DPs

09-10-30:
- Coccinelle: Coccinelle library v8.2-bool (09-10-26)
- Conversion/Coccinelle: convert CoLoR ATerm's into Coccinelle terms
  + definition of RPO on CoLoR ATerm's using Coccinelle RPO

09-10-19:
- Conversion/String_of_ATerm: convert a unary TRS into an SRS
- Term/WithArity/AReverse: reversal of unary TRSs

09-07-08:
- SemLab/AFlatCont: flat context closure
- SemLab/ARootLab: root labeling
- MannaNess/ARedPair: rule elimination using reduction pairs,
  functors building a reduction pair from a monotone algebra
  or an argument filtering

09-06-26:
- Util/Set/SetUtil: infinite sets
- Term/WithArity/ARules: rewriting with infinite sets of rules
- Term/WithArity/AMorphism: extended to infinite sets of rules
- SemLab/ASemLab: theorem of semantic labeling (with ordered labels)

09-06-19:
- simplified all function definitions on terms f such that the corresponding
  function on vectors is (Vmap f)
- Filter/AProj: arguments filtering with projections only

09-05-22:
- Term/WithArity/AUnary: properties of systems with unary symbols only
- Conversion/ATerm_of_String: equivalence of the well-foundedness of an SRS
  and of its translation as TRS
- NonTermin/AModLoop: definition and correctness proof of a boolean function
  checking that there is a loop in a relative TRS
- NonTermin/SLoop: definition and correctness proof of a boolean function
  checking that there is a loop in an SRS
- NonTermin/SModLoop: definition and correctness proof of a boolean function
  checking that there is a loop in a relative SRS

09-05-11: [Blanqui,Wang,Zhang]
- NonTermin/ALoop: definition and correctness proof of a boolean function
  checking that there is a loop in a TRS
- NatUtil: unicity of Euclidean division

09-05-07:
- Term/WithArity/AReduct: list of reducts of a term and proof that
  rewriting is finitely branching
- Term/WithArity/AMorphism: definitions and lemmas on algebra morphisms

09-05-07: [Blanqui,Wang,Zhang]
- added new definitions and lemmas on vectors (sub-vector Vsub, etc.)
- Term/WithArity/APosition: positions in a term and related functions
  and relations (subterm, replacement, context, rewriting)

09-04-29:
- added (ordered) semi-rings, matrices and matrix interpretations on BigN
- removed antisymmetry and irreflexivity assumptions for ordered semi-rings

09-04-24: [Koprowski]
- added a framework for checking whether a given certificate is a correct
  termination proof for a given problem. This check is done by a Coq
  function (no Ltac), so it should be possible to extract from it
  a certified termination proof checker.
- added support for polynomial interpretations in the new proof
  checker framework.

09-04-17:
- extended semi-rings, matrices and matrix interpretations on setoids
- added boolean function for testing integer equality since the one
  defined in Coq is too complex and uses an opaque lemma

09-04-13: [Strub]
- Term/WithArity/AMatching: correct and complete matching algorithm
- Util/FMap/FMapUtil: bundle for FMap definitions + properties

09-03-18:
- decidability of equality on symbols and terms are replaced
  by boolean functions

-----------------------------------------------------------------------------
09-03-11: NEW RELEASE

09-01-22: [Koprowski]
- HORPO: beta-reduction included into HORPO; added examples, including
  an example illustrating non-transitivity of HORPO

08-10-31:
- Term/WithArity/AUnif: termination and completeness of the syntactic
  unification algorithm
- DP/ADPUnif: correctness of the over DP graph based on unification

08-08-07:
- Util/Relation/OrdDec: type totally ordered with a comparison function
- Util/List/ListDec: boolean functions on lists using a boolean equality test
- DP/ADecomp: proof that termination follows from any valid decomposition
  of an over DP graph and the termination of each component
- Term/WithArity/ATrsNorm: canonical representation of lists of rules

08-05-15:
- Util/FSet/FSetUtil: lemmas and tactics on Coq FSet's
- Term/WithArity/AVariables: set of variables in a term (based on FSet)
  and properties wrt substitution
- Term/WithArity/AUnif: correctness of a syntactic unification algorithm

08-03-14: [Koprowski, Waldmann]
added support for arctic matrix interpretations proofs;
unified with development on matrix interpretations
- MatrixInt/*
- Util/Algebra/SemiRing
- Util/Algebra/OrdSemiRing

08-02-13:
- Term/String/SReverse: SRS inversion preserves termination

08-01-23:
added support for boolean reasoning and boolean functions testing equality
- Util/Bool/BoolUtil
- Util/List/ListUtil
- Term/Varyadic/VTerm

07-08-23: [Lucas] added SCC decomposition (SCC = Strongly Connected Component)
- Util/List/SortUtil: lemmas on list sorting
- Util/Nat/log2: definition and properties of log2 and exp2
- Util/Nat/BoundNat: type of natural numbers smaller than some constant
- DP/AGraph: generalization of the notion of DP graph
- DP/HDE: simple over DP graph based on head symbol equality
- Util/Relation/SCC: definition of SCC and basic properties
- Util/Relation/AdjMat: adjacency matrix of a finite relation on N
- Util/Relation/GDomainBij: bijection between a set of n elements
  and the set of integers 0 .. n-1
- Util/Relation/SCC_dec: decidability of SCC decomposition
- Util/Relation/SCCTopoOrdering: topological ordering on SCCs
- DP/SCCunion: termination based on SCC decomposition

07-08-06: added support for classical reasoning
- Util/Logic/ClassicUtil: basic meta-theorems of classical logic
- Util/Logic/DepChoice: axiom of dependent choice
- Util/Logic/DepChoicePrf: proof of the axiom of dependent choice
  using classical logic and the axiom of choice
- Util/Relation/NotSN: properties of ~SN terms in classical logic
- Util/Relation/NotSN_IS: ~SN terms give infinite sequences
  using dependent choice and classical logic
- Util/Relation/RedLength: maximal reduction length of a term
  wrt a well-founded finitely branching relation
- Util/Relation/IS_NotSN: a well-founded finitely branching relation
  has no infinite sequence

07-05-25:
- Term/String: strings
- Conversion/ATerm_of_String: conversion strings -> algebraic terms

07-04-25: [Koprowski,Zantema]
- MatrixInt: matrix interpretations
- Util/Matrix: matrices
- Util/Algebra/SemiRing: semi-rings

-----------------------------------------------------------------------------
07-03-22: NEW RELEASE

07-02-16:
- Simplification of the compilation procedure

- DP/ADPGraph: proof of the DP criterion based on cycles

- Util/Relation/Union: union of two well-founded relations
- Util/Relation/SN: new general lemmas on termination
- Util/Relation/Iter: iteration of a relation

- Util/Relation/Total: total completion [Le Roux]
- Util/Relation/RelDec: decidability of relations [Le Roux]
- Util/Relation/Path: paths and sub-relations [Le Roux]

- Util/List/ListOccur: number of occurrences and pigeon-hole principle
- Util/List/ListRepeatFree: smallest prefix without duplication
- Util/List/ListShrink: new functions and lemmas on lists [Le Roux]

- Term/WithArity/ARename: variable renamings
- Term/WithArity/ASubstitution: added union of two substitutions

- Term/WithArity/ARelation: results on compatibility moved to ACompat
- Util/Relation/WfUtil renamed into AccUtil
- Various lemmas renamed with intro or elim suffix

06-12-04:
- MannaNess/AMannaNess: added rule elimination for relative termination
- Acc replaced by SN in various files
- Term/WithArity/ARedOrd moved to MannaNess/AMannaNess

06-12-01:
- Various modifications for compiling with the new version of Coq
- Util/Relation/SN: inductive definition of strong normalization
  (inverse of Coq accessibility)
- Util/Relation/RelUtil: practical notations and useful results
  on composition, union and reflexive and transitive closures
- Term/WithArity: elimination of useless hypotheses
  in AWFMInterpretation and ARedOrd
- Util/Relation/Lexico: new formalization of lexicographic ordering
  with minimal hypotheses
- Term/WithArity/ATrs: rewriting modulo the transitive closure of some relation
- Term/WithArity/ARedOrd: rule elimination for relative elimination

06-07-21:
- various updates for the first release of Rainbow
- Util/Multiset: parameter eqA_dec added to functor arguments
- RPO: the module structure has been flattened
- Util/Vector: V0_eq redefined with Vcast to make it computable
  (the previous version was using the axiom eq_rect_eq)
- Util/Polynom: tactics for monotony and termination [Hinderer]

-----------------------------------------------------------------------------
06-05-10: NEW RELEASE

06-05-10:
- HORPO: higher-order recursive path ordering [Koprowski]
- Term/SimpleType: simply typed lambda-terms with de Bruijn indices [Koprowski]
- Util/List: more functions and lemmas (nth element, initial segment, etc.)
- Util/Multiset: a few modifications and additions (decidability, etc.)

06-01-10:
- RPO: recursive path ordering with statuses [Coupet-Grimal,Delobel]
- Util/Multiset: additions in MultisetOrder, MultisetListOrder
- Util/List: additions in ListUtil
- Util/Relation: additions in WfUtil
- MPO/VMPO: elimination of irreflexivity hypothesis
- Util/Multiset/MultisetListOrder:
  elimination of transitivity hypothesis in HAccTermsToTermlist
- Util/List: creation of LexicographicOrder
- Util/Relation: creation of Preorder

05-12-06:
- Conversion/VTerm_of_ATerm: conversion from algebraic terms to varyadic terms
- Term/Varyadic: creation of VContext, VSubstitution, VTrs

05-10-07:
- MPO: multiset path ordering [Coupet-Grimal,Delobel]
- Term/Varyadic: terms without arity
- Util/Multiset: creation of MultisetListOrder
- Util/Multiset: proof of Acc_iso in MultisetAuxiliary
- Util: additions in Multiset

05-09-19:
- License: CeCILL version 2
- Util/Multiset: finite multisets and proof that the multiset extension
  of an ordering preserves well-foundedness [Koprowski]
- Util: creation of Bool/BoolUtil, Pair/PairUtil, Logic/EqUtil
- Util: additions in ListUtil, LogicUtil

05-06-10:
- Filter: arguments filtering
- Term/WithArity: bug fixed in ARedOrd.v/manna_ness2
- Term/WithArity: renamings in ARelation
- Term/WithArity: additions in ARelation, ASubstitution, ATrs, ARedOrd
- Util/Vector: creation of VecBool, VecFilter
- Util: additions in LogicUtil, NatUtil, RelUtil, WfUtil, VecUtil

-----------------------------------------------------------------------------
05-03-14: NEW RELEASE

05-03-14:
- Util/Vector: library on vectors
- Util/Polynom: library on integer polynomials with multiple variables
- Term/WithArity: library on algebraic terms with symbols of fixed arity
- PolyInt: proof of the termination criterion based on polynomial
  interpretations [Hinderer]
- DP: proof of the fundamental dependency pairs theorem