Release of version 2.6

Dependencies

• Coq 8.17.1 or later
• Mathematical Components 1.17.0 or 1.18.0
• Coquelicot 3.4.0 or later

Main change from version 2.5 to version 2.6

• Modified the code to be compatible with CoqPlatform.2023.03.

Release of version 2.5

Dependencies

• Coq 8.13 or later
• Mathematical Components 1.15.0
• Coquelicot 3.1.0 or later

Main changes from version 2.4 to version 2.5

• Modified the code to be compatible with Mathematical Components 1.15.0.
• Added the information of reference to some documents.

Release of version 2.4

Dependencies

• Coq 8.13 or later
• Mathematical Components 1.14.0
• Coquelicot 3.1.0 or later

Main changes from version 2.3 to version 2.4

• The reviewed paper is added to Actuary/doc.

Release of version 2.3

Dependencies

• Coq 8.13 or later
• Mathematical Components 1.12.0 or later
• Coquelicot 3.1.0 or later

Main changes from version 2.2 to version 2.3

• A new example is added to Examples.v.

Release of version 2.2

Dependencies

• Coq 8.13 or later
• Mathematical Components 1.12.0 or later
• Coquelicot 3.1.0 or later

Main changes from version 2.1 to version 2.2

• Some obsolete tactics are modified thanks to Karl Palmskog.
• The preprint (in Japanese) on this package is uploaded.
• Files are organized into theories and doc directories.

Release of version 2.1

Dependencies

• Coq: v8.13.2
• MathComp: 1.12.0
• Coquelicot: 3.1.0

Main changes from version 2.0 to version 2.1

• The basic standard build scripts are added thanks to Karl Palmskog.

Release of version 2.0

Dependencies

• Coq: v8.13.2
• MathComp: 1.12.0
• Coquelicot: 3.1.0

Main changes from version 1.0 to version 2.0

• Inequalities ">" and ">=" are replaced with "<" and "<=" (advice from ZulipChat).
• The force of mortality is formalized.
• Notations "δ", "ω" are changed to "\δ", "\ω" respectively.
• Some basic lemmas are taken in the "auto" tactic by "Hint Resolve".
• Generalized the frequency of payments in Premium.v. and Reserve.v.
• The continuous payment case is newly formalized.

Release of version 1.0

Dependencies

• Coq: v8.13.0
• MathComp: 1.12.0
• Coquelicot: 3.1.0