Taming 'auto with zarith' (for Coq PR #9856) (!8) · Merge requests · Flocq / flocq

BESSON Frederic requested to merge fbesson/flocq:master into master Apr 26, 2019

With PR #9856, zify is using existing positivity hypotheses from the context. This has the side-effect of improving (just a little bit) auto with zarith which in turn breaks a few proofs.

NB: tested with 8.10+alpha and 8.8

Taming 'auto with zarith' (for Coq PR #9856)

Merge request reports