| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-17 | (Partial) fix for bug #4453: raise an error instead of an anomaly. | Matthieu Sozeau | |
| 2015-12-17 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-15 | Extraction: more cautious use of intermediate result caching (fix #3923) | Pierre Letouzey | |
| During an extraction, a few tables are maintained to cache intermediate results. Due to modules, the kernel_name index for these caching tables aren't enough. For instance, in bug #3923, a constant is first transparent (from inside the module) then opaque (when seen from the signature). The previous protections were actually obsolete (tests via visible_con), we now checks that the constant_body is still the same. | |||
| 2015-12-15 | Fix test-suite files after change in refine tactic. | Maxime Dénès | |
| Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c. | |||
| 2015-12-15 | Refine tactic now shelves unifiable holes. | Pierre-Marie Pédrot | |
| The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet. | |||
| 2015-12-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-14 | Test file for #4363 was not complete. | Maxime Dénès | |
| 2015-12-11 | Univs: Fix bug #4363, nested abstract. | Matthieu Sozeau | |
| 2015-12-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-03 | Univs: fix bug #4443. | Matthieu Sozeau | |
| Do not substitute rigid variables during minimization, keeping their equality constraints instead. | |||
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | |
| 2015-11-30 | Test for bug #4149. | Pierre-Marie Pédrot | |
| 2015-11-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-28 | Test-suite files for closed bugs | Matthieu Sozeau | |
| 2015-11-28 | Closed bugs. | Matthieu Sozeau | |
| 2015-11-27 | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau | |
| 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. | |||
| 2015-11-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-19 | Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-11-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-12 | Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms. | Pierre-Marie Pédrot | |
| We retypecheck the hypotheses introduced by the refine primitive instead of blindly trusting them when the unsafe flag is set to false. | |||
| 2015-11-12 | Fixed test-suite file for bug #3998. | Matthieu Sozeau | |
| 2015-11-11 | 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 | |
| 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 | 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-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-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 | 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 | 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 | Univs: fix bug #4375, accept universe binders on (co)-fixpoints | Matthieu Sozeau | |
| 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-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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |