coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-04-28	[test-suite] Remove a test with a Timeout that fails frequently on CI.	Théo Zimmermann

2018-09-25	Remove romega	Vincent Laporte

2017-06-16	romega: avoid potential slowdown when changing concl by reified version	Pierre Letouzey
	On some benchmarks provided by Chantal Keller a long time ago, romega was abnormally slow compared to omega (or lia). It turned out that the change of concl by reified version was triggering unnecessary unfolds of Z.add, instead of unfolding ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by the various Parameter Inline : no more indirections, Z_as_Int.plus is directly Z.add. Also use Tactics.convert_concl_no_check for this "change", as recommended by PMP.