| bdb702d | Pierre Roux | 01 February 2024, 10:26:39 UTC | Merge pull request #203 from coq-community/coq_18590 Adapt to https://github.com/coq/coq/pull/18590 | 01 February 2024, 10:26:39 UTC |
| 9ed2c9f | Pierre Roux | 01 February 2024, 10:14:17 UTC | Adapt to https://github.com/coq/coq/pull/18590 | 01 February 2024, 10:14:17 UTC |
| 79e7ee7 | Bas Spitters | 10 November 2023, 09:36:45 UTC | Merge pull request #202 from Villetaneuse/rm_arith_files Adapt to Coq/Coq#18164 | 10 November 2023, 09:36:45 UTC |
| 7d6c53e | Pierre Rousselin | 10 November 2023, 08:49:01 UTC | Compatibility with 8.14 and 8.15 A lemma has been added to CLogic.v because of the lack of Nat.Even_Odd_dec in 8.14. | 10 November 2023, 08:49:01 UTC |
| 5c94a75 | Pierre Rousselin | 08 November 2023, 11:47:54 UTC | Adapt to Coq/Coq#18164 | 08 November 2023, 11:47:54 UTC |
| a6158dc | Théo Zimmermann | 16 October 2023, 15:39:53 UTC | Merge pull request #201 from coq-community/coq-8.18 Update testing to Coq 8.18. | 16 October 2023, 15:39:53 UTC |
| fbb6324 | Théo Zimmermann | 16 October 2023, 14:43:00 UTC | Update testing to Coq 8.18. | 16 October 2023, 14:43:00 UTC |
| f865fa8 | Pierre Roux | 05 October 2023, 14:22:45 UTC | Merge pull request #199 from coq-community/master+adapting-cast-using-scope-bound-to-type Adapting to interpretation of (x:T) now activating scope for T if any. | 05 October 2023, 14:22:45 UTC |
| 6641c67 | Pierre Roux | 26 September 2023, 09:06:27 UTC | Adapting to interpretation of (x:T) now activating scope for T if any. These were situations where the cast was needed to hint type class inference but the body was expected to be interpreted in the type-class (current) scope rather than in the more specialized scope bound to the cast type. We add a "%mc" to force using the type-class based generic interpretation. | 26 September 2023, 09:06:27 UTC |
| c08a041 | Bas Spitters | 31 May 2023, 18:02:48 UTC | Merge pull request #198 from anandadalton/deprecations Remove deprecated options/flags | 31 May 2023, 18:02:48 UTC |
| cba97fd | Ana Dalton | 31 May 2023, 15:37:03 UTC | 'remove deprecated options/flags' | 31 May 2023, 15:37:03 UTC |
| 48735ca | Bas Spitters | 31 May 2023, 14:02:47 UTC | Merge pull request #197 from anandadalton/configure_sh Remove conditional from configure.sh | 31 May 2023, 14:02:47 UTC |
| ae9ab3a | Ana Dalton | 30 May 2023, 20:55:17 UTC | Revert "'Deprecate Nat.mod_add for Nat.Div0.mod_add'" This reverts commit 7e39c789778465b5f785d211827731cfdb4529c6. Nat.Div0 modules are too modern for versions of Coq 8.16 and below. | 30 May 2023, 20:55:17 UTC |
| a3e9b98 | Ana Dalton | 30 May 2023, 20:48:04 UTC | Revert "'Deprecate Nat.div_le_mono for Div0.div_le_mono'" This reverts commit 09f771924e911acd5fb3d2fea8289980d9ea0ec8. It seems that older versions of Coq do not have these modules and therefore this is a breaking change. I do not know why CI didn't catch this. | 30 May 2023, 20:48:04 UTC |
| 551189e | Ana Dalton | 30 May 2023, 20:09:05 UTC | Remove conditional from configure.sh The conditional doesn't work in all bashes (doesn't work in mine, GNU bash, version 5.2.15(1)-release (x86_64-pc-linux-gnu) Moreover we don't even support versions of Coq that low anymore, so there's no need. | 30 May 2023, 20:09:05 UTC |
| ca47307 | Bas Spitters | 26 May 2023, 09:50:49 UTC | Merge pull request #195 from anandadalton/easy_fixes Deprecating notation | 26 May 2023, 09:50:49 UTC |
| 36fd7af | Ana Dalton | 25 May 2023, 22:09:14 UTC | Deprecate beq_nat for Nat.eqb. | 25 May 2023, 22:09:14 UTC |
| 58840fd | Ana Dalton | 25 May 2023, 22:05:30 UTC | 'Deprecate lt_pred for Nat.lt_succ_lt_pred' | 25 May 2023, 22:05:30 UTC |
| dcb4183 | Ana Dalton | 25 May 2023, 21:57:49 UTC | 'Deprecate gt_trans for Nat.lt_trans' | 25 May 2023, 22:03:54 UTC |
| 820ba57 | Ana Dalton | 25 May 2023, 21:49:15 UTC | 'Deprecate le_plus_minus_r for Nat.sub_add' | 25 May 2023, 21:55:24 UTC |
| 8f62895 | Ana Dalton | 25 May 2023, 21:47:17 UTC | 'Deprecate plus_gt_compat_l for Nat.add_lt_mono_l' | 25 May 2023, 21:47:17 UTC |
| 23a9006 | Ana Dalton | 25 May 2023, 21:45:11 UTC | 'Deprecate gt_not_le for Nat.lt_nge' | 25 May 2023, 21:45:11 UTC |
| 85e4feb | Ana Dalton | 25 May 2023, 21:40:00 UTC | 'Deprecate mult_lt_compat_r for Nat.mul_lt_mono_pos_r' | 25 May 2023, 21:44:27 UTC |
| 0b31faf | Ana Dalton | 25 May 2023, 20:33:06 UTC | 'Deprecate Le.le_S_n for Nat.succ_le_mono' | 25 May 2023, 21:22:02 UTC |
| 60b7a1f | Ana Dalton | 25 May 2023, 19:22:46 UTC | 'Deprecate le_not_gt for Nat.le_ngt' | 25 May 2023, 20:14:53 UTC |
| 9ddb260 | Ana Dalton | 25 May 2023, 19:08:36 UTC | 'Deprecate plus_le_reg_l for Nat.add_le_mono_l' | 25 May 2023, 19:08:36 UTC |
| a0c28b6 | Ana Dalton | 25 May 2023, 16:55:36 UTC | 'Deprecate plus_lt_compat_l for Nat.add_lt_mono_l' | 25 May 2023, 16:55:36 UTC |
| 3e0d10b | Ana Dalton | 25 May 2023, 16:41:45 UTC | 'Deprecate plus_le_compat_l for Nat.add_le_mono_l' | 25 May 2023, 16:41:45 UTC |
| 07d89c5 | Ana Dalton | 25 May 2023, 16:27:50 UTC | 'Deprecate plus_lt_reg_l for Nat.add_lt_mono_l' | 25 May 2023, 16:27:50 UTC |
| c1f3a5d | Ana Dalton | 24 May 2023, 21:54:42 UTC | 'Deprecate not_le_minus_0 for Nat.sub_0_le' | 24 May 2023, 23:20:17 UTC |
| 404f96e | Ana Dalton | 24 May 2023, 21:20:07 UTC | 'Deprecate minus_n_O for Nat.sub_0_r' | 24 May 2023, 21:40:38 UTC |
| e50610b | Ana Dalton | 24 May 2023, 20:27:22 UTC | 'Deprecate lt_pred_n_n for Nat.lt_pred_l' | 24 May 2023, 20:57:00 UTC |
| 43d60e1 | Ana Dalton | 24 May 2023, 20:26:23 UTC | Deprecate minus_plus for Nat.add_sub. | 24 May 2023, 20:26:23 UTC |
| b446ae7 | Bas Spitters | 24 May 2023, 19:08:47 UTC | Merge pull request #194 from anandadalton/easy_fixes Deprecated notations | 24 May 2023, 19:08:47 UTC |
| 2a7c386 | Ana Dalton | 24 May 2023, 18:21:18 UTC | Merge branch 'coq-community:master' into easy_fixes | 24 May 2023, 18:21:18 UTC |
| e275fc7 | Ana Dalton | 24 May 2023, 17:49:14 UTC | 'Deprecate lt_le_S for Nat.le_succ_l' | 24 May 2023, 18:17:55 UTC |
| e28ce44 | Ana Dalton | 24 May 2023, 16:13:41 UTC | 'Deprecate lt_O_neq for Nat.neq_0_lt_0' | 24 May 2023, 18:17:55 UTC |
| 7e39c78 | Ana Dalton | 23 May 2023, 22:59:07 UTC | 'Deprecate Nat.mod_add for Nat.Div0.mod_add' | 24 May 2023, 18:17:55 UTC |
| 5735f42 | Ana Dalton | 23 May 2023, 22:30:56 UTC | 'Deprecate le_lt_n_Sm for Nat.lt_succ_r' | 24 May 2023, 18:17:55 UTC |
| f41ab4f | Ana Dalton | 23 May 2023, 21:12:51 UTC | 'Deprecate minus_n_n for Nat.sub_diag' | 24 May 2023, 17:43:53 UTC |
| 7a5dc70 | Ana Dalton | 23 May 2023, 19:46:21 UTC | 'Deprecate lt_S_n for Nat.succ_lt_mono' | 24 May 2023, 17:43:53 UTC |
| aa3859d | Ana Dalton | 23 May 2023, 19:30:38 UTC | 'Deprecate Zdiv_eucl_POS for Coq.ZArith.BinIntDef.Z.pos_div_eucl' | 24 May 2023, 17:43:53 UTC |
| 6521bf9 | Ana Dalton | 23 May 2023, 19:15:50 UTC | 'Deprecate le_Sn_le for Nat.lt_le_incl' | 24 May 2023, 17:43:53 UTC |
| 5b31252 | Ana Dalton | 22 May 2023, 23:35:22 UTC | 'Deprecate le_n_O_eq for Nat.le_0_r' | 24 May 2023, 17:43:53 UTC |
| 024db94 | Ana Dalton | 22 May 2023, 18:25:35 UTC | 'Deprecate neq_O_lt for Nat.neq_0_lt_0' | 24 May 2023, 17:43:53 UTC |
| e358180 | Bas Spitters | 22 May 2023, 19:22:42 UTC | Merge pull request #191 from anandadalton/easy_fixes More deprecations of notation | 22 May 2023, 19:22:42 UTC |
| 7763ce1 | Ana Dalton | 22 May 2023, 17:14:53 UTC | 'Deprecate le_plus_minus for Nat.sub_add' | 22 May 2023, 17:51:10 UTC |
| ad827d3 | Bas Spitters | 20 May 2023, 06:11:48 UTC | Merge pull request #190 from anandadalton/easy_fixes Deprecate le_not_lt for Nat.le_ngt | 20 May 2023, 06:11:48 UTC |
| 09f7719 | Ana Dalton | 20 May 2023, 04:38:36 UTC | 'Deprecate Nat.div_le_mono for Div0.div_le_mono' | 20 May 2023, 04:59:51 UTC |
| 4fccdc0 | Ana Dalton | 20 May 2023, 04:17:38 UTC | 'Deprecate minus_Sn_m for Nat.sub_succ_l' | 20 May 2023, 04:36:05 UTC |
| 0cfee05 | Ana Dalton | 20 May 2023, 04:03:22 UTC | 'Deprecate Zmod for Z.modulo' | 20 May 2023, 04:03:22 UTC |
| 79d5b5f | Ana Dalton | 20 May 2023, 02:47:54 UTC | 'Deprecate lt_not_le for Nat.lt_nge' | 20 May 2023, 03:12:36 UTC |
| e9affa7 | Ana Dalton | 20 May 2023, 01:38:00 UTC | 'Deprecate lt_n_S for Nat.succ_lt_mono' | 20 May 2023, 02:37:10 UTC |
| 414d996 | Ana Dalton | 20 May 2023, 00:31:52 UTC | 'Deprecate le_not_lt for Nat.le_ngt' | 20 May 2023, 01:22:15 UTC |
| afa55ac | Bas Spitters | 19 May 2023, 11:57:34 UTC | Merge pull request #189 from anandadalton/easy_fixes More notation deprecations. | 19 May 2023, 11:57:34 UTC |
| 43c954b | Ana Dalton | 19 May 2023, 02:41:18 UTC | Deprecate lt_n_Sm_le by Nat.lt_succ_r. This change separates out instances where the substitution is a bit clunkier: we have to do lt_n_Sm_le i j H => proj1 (Nat.lt_succ_r i j) H instead. | 19 May 2023, 02:41:18 UTC |
| 5a1f8de | Ana Dalton | 18 May 2023, 16:02:12 UTC | Simple deprecations of lt_n_Sm_le. The notation lt_n_Sm_le is deprecated for Nat.lt_succ_r, but Nat.lt_succ_r is not a drop-in replacement for lt_n_Sm_le. This means that e.g. in "./algebra/Bernstein.v", replacing lt_n_Sm_le is not so easy, because lt_n_Sm_le is used as an argument to other proof terms. | 18 May 2023, 16:02:12 UTC |
| 40b0790 | Bas Spitters | 18 May 2023, 08:34:58 UTC | Merge pull request #188 from anandadalton/easy_fixes More fixes for deprecated notation warnings | 18 May 2023, 08:34:58 UTC |
| 02a251c | Ana Dalton | 17 May 2023, 21:47:46 UTC | Deprecate S_pred for Nat.lt_succ_pred. | 17 May 2023, 21:47:46 UTC |
| 81dd60d | Ana Dalton | 17 May 2023, 16:54:11 UTC | 'Deprecate lt_div2 for Nat.lt_div2' | 17 May 2023, 17:19:37 UTC |
| 0ac52c5 | Ana Dalton | 17 May 2023, 16:54:11 UTC | 'Deprecate lt_asym for Nat.lt_asymm' | 17 May 2023, 17:19:37 UTC |
| be424b0 | Ana Dalton | 17 May 2023, 16:54:11 UTC | 'Deprecate plus_lt_le_compat for Nat.add_lt_le_mono' | 17 May 2023, 17:19:14 UTC |
| 0b3e5a8 | Ana Dalton | 17 May 2023, 16:54:11 UTC | 'Deprecate le_or_lt for Nat.le_gt_cases' | 17 May 2023, 17:19:14 UTC |
| e8e6681 | Ana Dalton | 17 May 2023, 16:54:11 UTC | 'Deprecate minus_diag for Nat.sub_diag' | 17 May 2023, 17:19:14 UTC |
| cbac029 | Ana Dalton | 17 May 2023, 16:54:11 UTC | 'Deprecate mult_0_r for Nat.mul_0_r' | 17 May 2023, 17:19:14 UTC |
| 3ff7357 | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate mult_1_l for Nat.mul_1_l' | 17 May 2023, 17:19:14 UTC |
| 6b0b56b | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate mult_assoc for Nat.mul_assoc' | 17 May 2023, 17:19:14 UTC |
| e3915ef | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate Lt.le_lt_or_eq_iff for Nat.lt_eq_cases' | 17 May 2023, 17:19:14 UTC |
| d10c584 | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate mult_1_r for Nat.mul_1_r' | 17 May 2023, 17:19:14 UTC |
| 8fbb818 | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate plus_Snm_nSm for Nat.add_succ_comm' | 17 May 2023, 17:19:14 UTC |
| 8f55e9c | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate max_l for Nat.max_l' | 17 May 2023, 17:19:14 UTC |
| fc77a5c | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate mult_le_compat for Nat.mul_le_mono' | 17 May 2023, 17:19:14 UTC |
| 5767ba1 | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate max_r for Nat.max_r' | 17 May 2023, 17:19:14 UTC |
| ef81c7f | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate le_pred for Nat.pred_le_mono' | 17 May 2023, 17:19:14 UTC |
| 1aa0568 | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate max_assoc for Nat.max_assoc' | 17 May 2023, 17:19:14 UTC |
| 2fab72e | Ana Dalton | 17 May 2023, 16:54:10 UTC | 'Deprecate plus_le_compat for Nat.add_le_mono' | 17 May 2023, 17:19:14 UTC |
| a9e908b | Ana Dalton | 17 May 2023, 16:54:09 UTC | 'Deprecate le_Sn_O for Nat.nle_succ_0' | 17 May 2023, 17:19:13 UTC |
| 3f14199 | Ana Dalton | 17 May 2023, 16:54:09 UTC | 'Deprecate le_pred_n for Nat.le_pred_l' | 17 May 2023, 17:19:13 UTC |
| eebdbd8 | Ana Dalton | 17 May 2023, 16:54:09 UTC | 'Deprecate max_comm for Nat.max_comm' | 17 May 2023, 17:19:13 UTC |
| 728e852 | Ana Dalton | 17 May 2023, 16:54:09 UTC | 'Deprecate lt_n_O for Nat.nlt_0_r' | 17 May 2023, 17:19:13 UTC |
| 19dd0d7 | Ana Dalton | 17 May 2023, 16:54:09 UTC | 'Deprecate lt_irrefl for Nat.lt_irrefl' | 17 May 2023, 17:19:04 UTC |
| c073b42 | Ana Dalton | 17 May 2023, 16:54:09 UTC | 'Deprecate plus_0_l for Nat.add_0_l' | 17 May 2023, 16:54:09 UTC |
| 6f80837 | Ana Dalton | 17 May 2023, 16:54:09 UTC | 'Deprecate le_antisym for Nat.le_antisymm' | 17 May 2023, 16:54:09 UTC |
| bfa79eb | Ana Dalton | 17 May 2023, 16:54:09 UTC | 'Deprecate double for Nat.double' | 17 May 2023, 16:54:09 UTC |
| 5083846 | Ana Dalton | 17 May 2023, 16:45:36 UTC | 'Deprecate plus_permute for Nat.add_shuffle3' | 17 May 2023, 16:45:36 UTC |
| e3c52a8 | Ana Dalton | 17 May 2023, 16:45:36 UTC | 'Deprecate le_max_r for Nat.le_max_r' | 17 May 2023, 16:45:36 UTC |
| a2c766c | Ana Dalton | 17 May 2023, 16:44:29 UTC | 'Deprecate le_n_Sn for Nat.le_succ_diag_r' | 17 May 2023, 16:44:29 UTC |
| e31aa90 | Ana Dalton | 17 May 2023, 16:44:29 UTC | 'Deprecate le_max_l for Nat.le_max_l' | 17 May 2023, 16:44:29 UTC |
| 8b201ae | Ana Dalton | 17 May 2023, 16:42:45 UTC | 'Deprecate lt_O_Sn for Nat.lt_0_succ' | 17 May 2023, 16:42:45 UTC |
| 8394538 | Bas Spitters | 17 May 2023, 07:53:23 UTC | Merge pull request #187 from anandadalton/easy_fixes Remove more deprecated notations | 17 May 2023, 07:53:23 UTC |
| 4b0497c | Ana Dalton | 17 May 2023, 06:21:49 UTC | 'Deprecate mult_le_compat_r for Nat.mul_le_mono_r' | 17 May 2023, 07:02:24 UTC |
| 50e3c39 | Ana Dalton | 17 May 2023, 06:21:49 UTC | 'Deprecate le_Sn_0 for Nat.nle_succ_0' | 17 May 2023, 07:02:24 UTC |
| 81eab46 | Ana Dalton | 17 May 2023, 06:21:28 UTC | Deprecate min for Nat.min | 17 May 2023, 07:02:24 UTC |
| 208beb3 | Ana Dalton | 17 May 2023, 06:00:06 UTC | 'Deprecate le_Sn_n for Nat.nle_succ_diag_l' | 17 May 2023, 07:02:24 UTC |
| c4a60fa | Ana Dalton | 17 May 2023, 05:25:32 UTC | Deprecate le_plus_l to Nat.le_add_r | 17 May 2023, 07:02:24 UTC |
| d4e07ca | Ana Dalton | 17 May 2023, 05:23:38 UTC | Deprecate mult_comm to Nat.mul_comm | 17 May 2023, 07:02:24 UTC |
| 93de4c0 | Ana Dalton | 17 May 2023, 05:05:59 UTC | Deprecate plus_comm for Nat.add_comm | 17 May 2023, 07:02:24 UTC |
| efeae70 | Ana Dalton | 17 May 2023, 04:37:24 UTC | Deprecate plus_assoc to Nat.add_assoc | 17 May 2023, 07:02:24 UTC |
| 5781f42 | Ana Dalton | 17 May 2023, 04:23:30 UTC | Deprecate plus_0_r for Nat.add_0_r | 17 May 2023, 07:02:24 UTC |
| d3a4c6b | Ana Dalton | 17 May 2023, 03:50:34 UTC | Deprecate le_0_n for Nat.le_0_l. | 17 May 2023, 07:02:15 UTC |
