aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2016-09-24Adding a test for bug #5096.Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-22Fixing #5095 (non relevant too strict test in let-in abstraction).Hugo Herbelin
2016-09-17Further "decide equality" tests on demand of Jason.Hugo Herbelin
2016-09-15Added a test file for contradiction.Hugo Herbelin
2016-09-15Continuing fix to #5078, taking also into account intropatterns.Hugo Herbelin
Getting closer from before when the bug was introduced + test.
2016-09-14Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-14Fixing test-suite after commit 43104a0b.Pierre-Marie Pédrot
2016-09-13test-suite/output-modulo-time made more robustEnrico Tassi
2016-09-12Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Hugo Herbelin
2016-09-12Merge remote-tracking branch 'github-coq/pr/249' into v8.6Matthieu Sozeau
2016-09-11Add support for testing output mod timing changesJason Gross
Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip numbers of seconds and to strip percentages. (This can potentially be extended later.) Add a test-suite file to make sure that LtacProf outputs some table.
2016-09-11Add a test for 4836Jason Gross
This required improving the machinery of the test-suite Makefile to support -compile.
2016-09-10Test for #5077.Hugo Herbelin
2016-09-09no-refold patchPaul Steckler
Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
2016-09-09Fix output test-suite after commit 0d3c319.Pierre-Marie Pédrot
2016-09-09Update csdp cache.Pierre-Marie Pédrot
This was making the test-suite fail on machines where csdp was not installed.
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
esprit d'escalier : is now also fixed for R
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail.
2016-09-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-07micromega : more robust generation of proof termsFrédéric Besson
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
2016-09-05Test file for #5065 - Anomaly: Not a proof by inductionMaxime Dénès
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-01Fix test-suite after Frédéric's 6231f07b2.Maxime Dénès
2016-08-31Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Frédéric Besson
If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
2016-08-31Fix bug #5043: [Admitted] lemmas pick up section variables.Pierre-Marie Pédrot
We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
2016-08-30Fixing output test-suite after warning for inner Requires.Pierre-Marie Pédrot
2016-08-30Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Pierre-Marie Pédrot
2016-08-30plugin micromega : nra also handles non-linear rational arithmetic over Q ↵Frédéric Besson
(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
2016-08-30Fix bug #3920: eapply masks an hypothesis name.Pierre-Marie Pédrot
The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch.
2016-08-28Fix bug #4764: Syntactic notation externalization breaks.Pierre-Marie Pédrot
2016-08-23Fix bug #4904: [Import] does not load intermediately unqualified names of ↵Pierre-Marie Pédrot
aliases.
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-20Fixing an anomaly in printing a unification error message.Hugo Herbelin
2016-08-19Test file for bug #4187.Pierre-Marie Pédrot
2016-08-19Merge remote-tracking branch 'origin/pr/246' into v8.6Matthieu Sozeau
2016-08-18Adding a test for bug #4653.Pierre-Marie Pédrot
2016-08-17Fixing #3070 ("subst" taking properly into account chains of dependencies).Hugo Herbelin
2016-08-16Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-29Fix bug #4673: regression in setoid_rewrite.Matthieu Sozeau
Modulo delta for types should be fully transparent.
2016-07-29Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-29Fix bug #3886, generation of obligations of fixesMatthieu Sozeau
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
2016-07-29Fix #4769, univ poly and elim schemes in sectionsMatthieu Sozeau
2016-07-26Fix bug #4754, allow conversion problems to remainMatthieu Sozeau
when checking that the rewrite relation is homogeneous in setoid_rewrite.
2016-07-21Fix bug #4679, weakened setoid_rewrite unificationMatthieu Sozeau
It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4.
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-19Fix Errors.out missing a dot...Matthieu Sozeau
2016-07-19Some extra fixes in printing patterns in binders.Hugo Herbelin
- typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
2016-07-19Taking into account binding patterns when agglutinating sequences of binders.Hugo Herbelin
Supporting accordingly printing of sequences of binders including binding patterns.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 04:06:28 +0000