| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-29 | Fix a bug in subst releaved by an OCaml warning. | Maxime Dénès | |
| 2016-09-29 | test-suite: fix sed on OS X, does not handle + | Matthieu Sozeau | |
| 2016-09-29 | Argument : assert does fail if no arg is given (fix #4864) | Enrico Tassi | |
| 2016-09-28 | Fix bug #4723 and FIXME in API for solve_by_tac | Matthieu Sozeau | |
| This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic. | |||
| 2016-09-28 | Typeclass backtracking example by J. Leivant | Matthieu Sozeau | |
| 2016-09-28 | Merge remote-tracking branch 'github/pr/232' into v8.6 | Maxime Dénès | |
| Was PR#232: Fix the parsing of goal selectors. | |||
| 2016-09-27 | Add fixed test-suite file for bug #4527 | Matthieu Sozeau | |
| 2016-09-27 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-26 | Unbreak Ltac [ | .. | ] notation in -compat 8.5 | Jason Gross | |
| Importing VectorNotations breaks `; []`. So we make sure it's not imported by defualt. Some files might be required to `Import VectorDef.VectorNotations` rather than just `Import VectorNotations`. | |||
| 2016-09-26 | Fix bug #4785 (use [ ] for vector nil) | Jason Gross | |
| Also delimit vector_scope with vector, so that people can write %vector without having to delimit it themselves. | |||
| 2016-09-26 | Posssible abstractions over goal variables when inferring match return clause. | Hugo Herbelin | |
| The no-inversion and maximal abstraction over dependencies now supports abstraction over goal variables rather than only on "rel" variables. In particular, it now works consistently using "intro H; refine (match H with ... end)" or "refine (fun H => match H with ... end)". By doing so, we ensure that all three strategies are tried in all situations where a return clause has to be inferred, even in the context of a "refine". See antepenultimate commit for discussion. | |||
| 2016-09-26 | Trying an abstracting dependencies heuristic for the match return clause ↵ | Hugo Herbelin | |
| even when no type constraint is given. This no-inversion and maximal abstraction over dependencies in (rel) variables heuristic was used only when a type constraint was given. By doing so, we ensure that all three strategies "inversion with dependencies as evars", "no-inversion and maximal abstraction over dependencies in (rel) variables", "no-inversion and no abstraction over dependencies" are tried in all situations where a return clause has to be inferred. See penultimate commit for discussion. | |||
| 2016-09-26 | Trying a no-inversion no-dependency heuristic for match return clause. | Hugo Herbelin | |
| The no-inversion no-dependency heuristic was used only in the absence of type constraint. We may now use it also in the presence of a type constraint. See previous commit for discussion. | |||
| 2016-09-26 | Fix bug #5093: typeclasses eauto depth arg does not accept a var. | Pierre-Marie Pédrot | |
| 2016-09-24 | Adding a test for bug #5096. | Pierre-Marie Pédrot | |
| 2016-09-23 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-23 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-22 | Fixing #5095 (non relevant too strict test in let-in abstraction). | Hugo Herbelin | |
| 2016-09-19 | Fixing test FunExt.v. | Hugo Herbelin | |
| 2016-09-19 | extensionality: Handle dependently-used hypotheses | Jason Gross | |
| 2016-09-19 | Adding an "extensionality in H" tactic which applies functional | Hugo Herbelin | |
| extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples. | |||
| 2016-09-17 | Further "decide equality" tests on demand of Jason. | Hugo Herbelin | |
| 2016-09-15 | Added a test file for contradiction. | Hugo Herbelin | |
| 2016-09-15 | Continuing fix to #5078, taking also into account intropatterns. | Hugo Herbelin | |
| Getting closer from before when the bug was introduced + test. | |||
| 2016-09-14 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-14 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-14 | Fixing test-suite after commit 43104a0b. | Pierre-Marie Pédrot | |
| 2016-09-13 | test-suite/output-modulo-time made more robust | Enrico Tassi | |
| 2016-09-12 | Fixing a recursive notation bug raised on coq-club on Sep 12, 2016. | Hugo Herbelin | |
| 2016-09-12 | Merge remote-tracking branch 'github-coq/pr/249' into v8.6 | Matthieu Sozeau | |
| 2016-09-11 | Add support for testing output mod timing changes | Jason 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-11 | Add a test for 4836 | Jason Gross | |
| This required improving the machinery of the test-suite Makefile to support -compile. | |||
| 2016-09-10 | Test for #5077. | Hugo Herbelin | |
| 2016-09-09 | no-refold patch | Paul 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-09 | Fix output test-suite after commit 0d3c319. | Pierre-Marie Pédrot | |
| 2016-09-09 | Update csdp cache. | Pierre-Marie Pédrot | |
| This was making the test-suite fail on machines where csdp was not installed. | |||
| 2016-09-08 | Fix Bug #5073 : regression of micromega plugin | Frédéric Besson | |
| esprit d'escalier : is now also fixed for R | |||
| 2016-09-08 | Fix Bug #5073 : regression of micromega plugin | Fré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-07 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-07 | micromega : more robust generation of proof terms | Fré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-05 | Test file for #5065 - Anomaly: Not a proof by induction | Maxime Dénès | |
| 2016-09-02 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-02 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-01 | Fix test-suite after Frédéric's 6231f07b2. | Maxime Dénès | |
| 2016-08-31 | Fix 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-31 | Fix 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-30 | Fixing output test-suite after warning for inner Requires. | Pierre-Marie Pédrot | |
| 2016-08-30 | Fix bug #4893: not_evar: unexpected failure in 8.5pl1. | Pierre-Marie Pédrot | |
| 2016-08-30 | plugin 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite