| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | bug fixes to vm computation + test cases. |  Gregory Malecha | 2015-12-09 |
| | | |||
| * | Fix some typos. |  Guillaume Melquiond | 2015-12-07 |
| | | |||
| * | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) |  Hugo Herbelin | 2015-12-05 |
| | | | | | | | | | based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal. | ||
| * | Univs: fix bug #4443. |  Matthieu Sozeau | 2015-12-03 |
| | | | | | | Do not substitute rigid variables during minimization, keeping their equality constraints instead. | ||
| * | Adding a target report to test-suite's Makefile to get a short summary. | Hugo Herbelin | 2015-12-02 |
| | | |||
| * | Improving syntax of pat/constr introduction pattern so that | Hugo Herbelin | 2015-12-02 |
| | | | | | | | pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though. | ||
| * | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | 2015-12-02 |
| | | |||
| * | Test for bug #4149. |  Pierre-Marie Pédrot | 2015-11-30 |
| | | |||
| * | Test-suite files for closed bugs |  Matthieu Sozeau | 2015-11-28 |
| | | |||
| * | Closed bugs. | Matthieu Sozeau | 2015-11-28 |
| | | |||
| * | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau | 2015-11-27 |
| | | | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere. | ||
| * | Fixing the "parsing rules with idents later declared as keywords" problem. | Hugo Herbelin | 2015-11-26 |
| | | | | | | | | The fix was actually elementary. The lexer comes with a function to compare parsed tokens against tokens of the parsing rules. It is enough to have this function considering an ident in a parsing rule to be equal to the corresponding string parsed as a keyword. | ||
| * | Fixing a vm_compute bug in the presence of let-ins among the | Hugo Herbelin | 2015-11-22 |
| | | | | | parameters of an inductive type. | ||
| * | Fixing a bug of adjust_subst_to_rel_context. | Hugo Herbelin | 2015-11-22 |
| | | |||
| * | Fixing kernel bug in typing match with let-ins in the arity. | Hugo Herbelin | 2015-11-22 |
| | | | | | | | | | | | Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in 8.5beta2 and 8.5beta3 from a Coq file because typing done while compiling "match" would serve as a protection. However exploitable by calling the kernel directly, e.g. from a plugin (but a plugin can anyway do what it wants by bypassing kernel type abstraction). Fixing similar error in pretyping. | ||
| * | Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5. | Pierre-Marie Pédrot | 2015-11-19 |
| | | | | | | | | | | | | The issue was due to the fact that unfold hints are given a priority of 4 by default. As eauto was now using hint priority rather than the number of goals produced to order the application of hints, unfold were almost always used too late. We fixed this by manually giving them a priority of 1 in the eauto tactic. Also fixed the relative order of proof depth w.r.t. hint priority. It should not be observable except for breadth-first search, which is seldom used. | ||
| * | Fixing logical bugs in the presence of let-ins in computiong primitive | Hugo Herbelin | 2015-11-18 |
| | | | | | | | | | | projections. - lift accounting for the record missing in computing the subst from fields to projections of the record - substitution for parameters should not lift the local definitions - typo in building the latter (subst -> letsubst) | ||
| * | Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms. | Pierre-Marie Pédrot | 2015-11-12 |
| | | | | | | We retypecheck the hypotheses introduced by the refine primitive instead of blindly trusting them when the unsafe flag is set to false. | ||
| * | Fixed test-suite file for bug #3998. | Matthieu Sozeau | 2015-11-12 |
| | | |||
| * | Now closed. | Matthieu Sozeau | 2015-11-11 |
| | | |||
| * | Fix bug #3257, setoid_reflexivity should fail if not completing the goal. | Matthieu Sozeau | 2015-11-11 |
| | | |||
| * | Fix bug #4293: ensure let-ins do not contain algebraic universes in | Matthieu Sozeau | 2015-11-11 |
| | | | | | their type annotation. | ||
| * | Fixing bug #3554: Anomaly: Anonymous implicit argument. | Pierre-Marie Pédrot | 2015-11-11 |
| | | | | | | | | 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. | ||
| * | Test for bug #4404. | Pierre-Marie Pédrot | 2015-11-10 |
| | | |||
| * | 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 |
| | | |||
| * | Fixing complexity file f_equal.v. | Hugo Herbelin | 2015-11-06 |
| | | |||
| * | Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan | Hugo Herbelin | 2015-11-06 |
| | | | | | | | | 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. | ||
| * | Add test-suite file for #4273. | Matthieu Sozeau | 2015-11-05 |
| | | |||
| * | Univs: missing checks in evarsolve with candidates and missing a | Matthieu Sozeau | 2015-11-04 |
| | | | | | whd_evar in refresh_universes. | ||
| * | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | 2015-11-04 |
| | | | | | inconsistent). | ||
| * | Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion | Matthieu Sozeau | 2015-11-04 |
| | | | | | is buggy in general. | ||
| * | Test file for #4397. |  Maxime Dénès | 2015-11-04 |
| | | |||
| * | 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 | 2015-11-02 |
| | | | | | make them rigid to disallow minimization. | ||
| * | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau | 2015-10-29 |
| | | | | | universes are declared correctly in the enclosing proofs evar_map's. | ||
| * | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin | 2015-10-29 |
| | | | | | | | presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger. | ||
| * | 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 | 2015-10-28 |
| | | | | | After all, let's target 8.6. | ||
| * | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau | 2015-10-27 |
| | | | | | structure. | ||
| * | Two test-suite files for bugs 3974 and 3975 |  Pierre Letouzey | 2015-10-26 |
| | | |||
| * | Backtracking on interpreting toplevel calls to exact in scope determined | Hugo Herbelin | 2015-10-24 |
| | | | | | | | | | | | | | | 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. | ||
| * | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin | 2015-10-22 |
| | | | | | Was introduced in b06d3badb (15 Jul 2015). | ||
| * | Bug #3956 is fixed. | Matthieu Sozeau | 2015-10-21 |
| | | |||
| * | Test for #4372 (anomaly in inversion in the presence of fake dependency). | Hugo Herbelin | 2015-10-19 |
| | | |||
| * | Fixing #4198 (continued): not matching within the inner lambdas/let-ins | Hugo Herbelin | 2015-10-18 |
| | | | | | | | | 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). | ||
| * | Test for bug #4325. | Pierre-Marie Pédrot | 2015-10-17 |
| | | |||
| * | Test file for #4346: Set is no longer of type Type | Maxime Dénès | 2015-10-15 |
| | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |
path: root/test-suite