coq/test-suite/success, branch master The formal proof system Merge PR #14041: Enable canonical fun _ => _ projections. 2021-04-23T14:48:49+00:00 coqbot-app[bot] 2021-04-23T14:48:49+00:00 d332bbc3c1118631eb8c935ba61a8d071a90428e Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer 
Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Enable canonical `fun _ => _` projections. 2021-04-22T07:16:22+00:00 Jan-Oliver Kaiser 2020-05-14T15:08:20+00:00 2cbc36c6ae4ca22e000dbb045c865f54a454aca3 






Merge PR #14050: Remove remote counter system
2021-04-14T16:19:19+00:00

coqbot-app[bot]

2021-04-14T16:19:19+00:00

00391bd681098132cc89c356d1d27334d257fc8b

Reviewed-by: gares
Ack-by: ppedrot
Ack-by: ejgallego





Reviewed-by: gares
Ack-by: ppedrot
Ack-by: ejgallego







Remove remote counter system
2021-04-14T10:54:38+00:00

Gaëtan Gilbert

2021-03-26T14:34:59+00:00

3efee577b4c92b38a987b40e555fae2c0a2023c4












[zify] More aggressive application of saturation rules
2021-04-12T20:03:30+00:00

BESSON Frederic

2021-03-31T20:16:50+00:00

8193ca191cc435c108a4842ae38a11d74c7c20a5

The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints.  The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.

Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once

Co-authored-by:  Andrej Dudenhefner  <mrhaandi>

Closes #12184, #11656





The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints.  The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.

Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once

Co-authored-by:  Andrej Dudenhefner  <mrhaandi>

Closes #12184, #11656







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

Jim Fehrle

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

d3a51ac24244f586dfeff1a93b68cb084370534e












Remove double induction tactic
2021-01-20T20:10:08+00:00

Jim Fehrle

2021-01-19T19:19:33+00:00

cd17f9bfad72fb8f8da486facd75ff8ceecebd24












Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction pattern
2021-01-19T12:40:39+00:00

Pierre-Marie Pédrot

2021-01-19T12:40:39+00:00

a85d8cb68f53667d13ae0b5210b5e3dcc3fd8aa4

Reviewed-by: ppedrot





Reviewed-by: ppedrot







Preventing internal temporary names to impact the "?H"-like intro-pattern names.
2021-01-18T14:42:00+00:00

Hugo Herbelin

2020-11-29T08:40:11+00:00

eb38680520811e7a5e64678719d7b57e87af1269












Fixes #13413: freshness issue with "%" introduction pattern.
2021-01-18T14:25:26+00:00

Hugo Herbelin

2020-11-28T14:10:21+00:00

e56c65cf68c4055b4e1272b5a2afbf5803d93a42

We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.





We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.