| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-11-11 | Fix bug #4293: ensure let-ins do not contain algebraic universes in | Matthieu Sozeau | |
| their type annotation. | |||
| 2015-11-11 | Fixing bug #3554: Anomaly: Anonymous implicit argument. | Pierre-Marie Pédrot | |
| We just handle unnamed implicits using a dummy name. Note that the implicit argument logic should still output warnings whenever the user writes implicit arguments that won't be taken into account, but I'll leave that for another time. | |||
| 2015-11-10 | Updating test-suite after Bracketing Last Introduction Pattern set by | Hugo Herbelin | |
| default. Interestingly, there is an example where it makes the rest of the proof less natural. Goal forall x y:Z, ... intros [y|p1[|p2|p2]|p1[|p2|p2]]. where case analysis on y is not only in the 2nd and 3rd case, is not anymore easy to do. Still, I find the bracketing of intro-patterns a natural property, and its generalization in all situations a natural expectation for uniformity. So, what to do? The following is e.g. not as compact and "one-shot": intros [|p1|p1]; [intros y|intros [|p2|p2] ..]. | |||
| 2015-11-10 | Revert "Fixing #1225: we now skip the canonically built binding contexts of" | Hugo Herbelin | |
| This reverts commit 07620386b3c1b535ee7e43306a6345f015a318f0. Very sorry not ready. | |||
| 2015-11-10 | Fixing #1225: we now skip the canonically built binding contexts of | Hugo Herbelin | |
| the return clause and of the branches in a "match", computing them automatically when using the "at" clause of pattern, destruct, ... In principle, this is a source of incompatibilities in the numbering, since the internal binders of a "match" are now skipped. We shall deal with that later on. | |||
| 2015-11-10 | Merge origin/v8.5 into trunk | Hugo Herbelin | |
| Did some manual merge in tactics/tactics.ml. | |||
| 2015-11-10 | Test for bug #4404. | Pierre-Marie Pédrot | |
| 2015-11-08 | Adapting output test inference.v after c23f0cab6 (experimenting | Hugo Herbelin | |
| printing the type of the defined term of a LetIn). | |||
| 2015-11-07 | Fixing output test Existentials.v after eec77191b. | Hugo Herbelin | |
| 2015-11-07 | Tests for syntax "Show id" and [id]:tac (shelved or not). | Hugo Herbelin | |
| 2015-11-07 | Merge remote-tracking branch 'origin/v8.5' into upstream-trunk | Hugo Herbelin | |
| - Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml | |||
| 2015-11-06 | Fixing complexity file f_equal.v. | Hugo Herbelin | |
| 2015-11-06 | Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan | Hugo Herbelin | |
| for reporting it. A "cut" was not appropriately chained on the second goal but on both goals, with the chaining on the first goal introducing noise. | |||
| 2015-11-05 | Add test-suite file for #4273. | Matthieu Sozeau | |
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-04 | Univs: missing checks in evarsolve with candidates and missing a | Matthieu Sozeau | |
| whd_evar in refresh_universes. | |||
| 2015-11-04 | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | |
| inconsistent). | |||
| 2015-11-04 | Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion | Matthieu Sozeau | |
| is buggy in general. | |||
| 2015-11-04 | Test file for #4397. | Maxime Dénès | |
| 2015-11-02 | Fix bug #4151: discrepancy between exact and eexact/eassumption. | Matthieu Sozeau | |
| 2015-11-02 | Refresh rigid universes as well, and in 8.4 compatibility mode, | Matthieu Sozeau | |
| make them rigid to disallow minimization. | |||
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-29 | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau | |
| universes are declared correctly in the enclosing proofs evar_map's. | |||
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin | |
| presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger. | |||
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-28 | Fix test suite after Matthieu's ed7af646f2e486b. | Maxime Dénès | |
| 2015-10-28 | test cases. | Gregory Malecha | |
| 2015-10-28 | Univs: fix bug #4375, accept universe binders on (co)-fixpoints | Matthieu Sozeau | |
| 2015-10-28 | Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" | Hugo Herbelin | |
| After all, let's target 8.6. | |||
| 2015-10-27 | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau | |
| structure. | |||
| 2015-10-26 | Two test-suite files for bugs 3974 and 3975 | Pierre Letouzey | |
| 2015-10-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-24 | Backtracking on interpreting toplevel calls to exact in scope determined | Hugo Herbelin | |
| by the type to prove (was introduced in 35846ec22, r15978, Nov 2012). Not only it does not work when exact is called via a Ltac definition, but, also, it does not scale easily to refine which is a TACTIC EXTEND. Ideally, one may then want to propagate scope interpretations through ltac variables, as well as supporting refine... See #4034 for a discussion. | |||
| 2015-10-22 | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin | |
| Was introduced in b06d3badb (15 Jul 2015). | |||
| 2015-10-21 | Bug #3956 is fixed. | Matthieu Sozeau | |
| 2015-10-21 | Removing test for bug #3956. | Pierre-Marie Pédrot | |
| It breaks test-suite of trunk since Matthieu's fixes for the soundness of polymorphic universes, and I am unsure of the expected semantics. We should reintroduce it later on when we understand better the issue of simply fix it once and for all. | |||
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-19 | Test for #4372 (anomaly in inversion in the presence of fake dependency). | Hugo Herbelin | |
| 2015-10-18 | Fixing #4198 (continued): not matching within the inner lambdas/let-ins | Hugo Herbelin | |
| of the return clause and of the branches (what assumed that the implementation preserves the invariant that the return predicate and the branches are in canonical [fun Δ => t] form, with Δ possibly containing let-ins). | |||
| 2015-10-17 | Test for bug #4325. | Pierre-Marie Pédrot | |
| 2015-10-16 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-10-15 | Test file for #4346: Set is no longer of type Type | Maxime Dénès | |
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-12 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-11 | Adding test for bug #4366. | Pierre-Marie Pédrot | |
| 2015-10-11 | Fixing test-suite | Hugo Herbelin | |
| 2015-10-11 | Fixing untimely unexpected warning "Collision between bound variables" (#4317). | Hugo Herbelin | |
| Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables. | |||
| 2015-10-11 | Refining 0c320e79ba30 in fixing interpretation of constr under binders | Hugo Herbelin | |
| which was broken after it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). Interpretation was corrected, but error message was damaged. | |||
| 2015-10-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite