coq/doc/changelog/04-tactics, branch master The formal proof system changelog entry for Ltac2 unify 2021-04-19T18:24:50+00:00 Samuel Gruetter 2021-04-19T18:24:50+00:00 1dffce05d5b7b26a890a9d0359e54946e661511b 






Remove the omega tactic and related options
2021-04-03T01:52:59+00:00

Jim Fehrle

2021-01-11T22:47:13+00:00

d3a51ac24244f586dfeff1a93b68cb084370534e












changelog for 8.13.2
2021-04-01T09:19:19+00:00

Enrico Tassi

2021-04-01T09:18:44+00:00

39e3201c01b1a8baec279ccdc7a8acb3a341c3dd












Properly expand projection parameters in Btermdn.
2021-03-30T19:46:12+00:00

Pierre-Marie Pédrot

2021-03-30T14:35:42+00:00

75fec5716327beb1e93f294b70d563300d8f81ec

The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.

We fix this by adding dummy parameter arguments on sight.

Fixes #14009: TC search failure with primitive projections.





The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.

We fix this by adding dummy parameter arguments on sight.

Fixes #14009: TC search failure with primitive projections.







Fix Ltac2 `Array.init` exponential overhead
2021-03-26T13:28:34+00:00

Jason Gross

2021-03-26T13:28:34+00:00

7e5dc9f830bc2cdbc3b8cc8b830adafc61660055

Previously, `Array.init` was computing the first element of the array
twice, resulting in exponential overhead in the number of recursive
nestings of `Array.init`.  Notably, since `Array.map` is implemented in
terms of `Array.init`, this exponential blowup shows up in any term
traversal based on `Array.map` over the arguments of application nodes.

Fixes #14011





Previously, `Array.init` was computing the first element of the array
twice, resulting in exponential overhead in the number of recursive
nestings of `Array.init`.  Notably, since `Array.map` is implemented in
terms of `Array.init`, this exponential blowup shows up in any term
traversal based on `Array.map` over the arguments of application nodes.

Fixes #14011







Fix #12011 ssreflect "rewrite in" with setoids
2021-03-04T00:11:19+00:00

Gaëtan Gilbert

2021-02-26T16:35:31+00:00

0cb04b50bfde83001e59cd74da77142b567706d9

ssreflect asks setoid rewrite to rewrite in goal
"forall_special_name_ : T, _other_name_"

Since this is a non dependent product, setoid rewrite converts that to
"impl T _other_name_" and must be taught to restore the special name
when unfolding impl.





ssreflect asks setoid rewrite to rewrite in goal
"forall_special_name_ : T, _other_name_"

Since this is a non dependent product, setoid rewrite converts that to
"impl T _other_name_" and must be taught to restore the special name
when unfolding impl.







Merge PR #13781: [micromega] Deprecate hopefully useless options and flags
2021-01-28T20:25:52+00:00

coqbot-app[bot]

2021-01-28T20:25:52+00:00

59dc4eb40e9512d95f73df7a6bc67edcb1907acd

Reviewed-by: Zimmi48
Ack-by: jfehrle





Reviewed-by: Zimmi48
Ack-by: jfehrle







Update doc/changelog/04-tactics/13781-deprecate_micromega_options.rst
2021-01-25T09:18:32+00:00

Frédéric Besson

2021-01-25T09:18:32+00:00

a3b78a289d5a061970136ce297b50ece1c13b0e4

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>




Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>






Merge PR #13762: Remove double induction tactic
2021-01-24T10:55:31+00:00

Pierre-Marie Pédrot

2021-01-24T10:55:31+00:00

0a6444c522c18c634fe1030436ea82f326bada9a

Ack-by: Zimmi48
Reviewed-by: ppedrot





Ack-by: Zimmi48
Reviewed-by: ppedrot







changelog
2021-01-22T21:24:12+00:00

BESSON Frederic

2021-01-22T21:24:12+00:00

45f3e5fcda47733a3f0bab42469244f1cbfa9d9b