| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-12 | Update test for #3363 now that Require is forbidden inside modules. | Maxime Dénès | |
| 2014-12-19 | Fixing wrong notation level in #3295. | Hugo Herbelin | |
| 2014-12-16 | #3828 is solved. | Hugo Herbelin | |
| 2014-12-16 | Moving #2447 (congruence) to fixed. | Hugo Herbelin | |
| 2014-12-11 | New reproduction cases for the test suite. | Xavier Clerc | |
| 2014-12-05 | Commits on evar-evar unification fixed HoTT_coq_106 and improved the | Hugo Herbelin | |
| status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted). | |||
| 2014-11-30 | Adding test for bug #3417. | Pierre-Marie Pédrot | |
| 2014-11-30 | Test for bug #3487. | Pierre-Marie Pédrot | |
| 2014-11-30 | Test of bug #3682. | Pierre-Marie Pédrot | |
| 2014-11-25 | Bug #3804 is actually closed (thanks to Jason Gross for the notification). | Xavier Clerc | |
| 2014-11-25 | Tweak some test cases. | Xavier Clerc | |
| 2014-11-24 | Adding test for bug #3248. | Pierre-Marie Pédrot | |
| 2014-11-21 | Cleaning up closed bugs in test-suite. | Pierre-Marie Pédrot | |
| 2014-11-14 | Add missing "Fail" to test case for bug #2814. | Xavier Clerc | |
| 2014-11-14 | Reproduction cases for the test suite. | Xavier Clerc | |
| 2014-11-08 | Test #3655 was failing due to an anomaly. Now it rather has to fail | Hugo Herbelin | |
| normally, so failure is now detected by removing the "Fail". | |||
| 2014-11-08 | Test fixed by PMP's commits from Oct 21. | Hugo Herbelin | |
| 2014-11-04 | test suite: some reproduction cases for recently-reported bugs. | Xavier Clerc | |
| 2014-11-03 | New bugs revealed fixed: #3408 by (probably) Maxime's commits | Hugo Herbelin | |
| on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459. | |||
| 2014-10-21 | More precise test for #3459. | Hugo Herbelin | |
| 2014-10-16 | Bug fixed by Hugo. | Matthieu Sozeau | |
| 2014-10-15 | Adding a timeout to bug #2447. | Pierre-Marie Pédrot | |
| 2014-10-15 | Fix for bug #3618. | Matthieu Sozeau | |
| Fix typeclass resolution which was considering as subgoals of a tactic application unrelated pre-existing undefined evars. | |||
| 2014-10-15 | Bug 3692 is fixed. | Matthieu Sozeau | |
| 2014-10-15 | Bug 3628 is fixed. | Matthieu Sozeau | |
| 2014-10-03 | Add a bunch of reproduction files for bugs. | Xavier Clerc | |
| 2014-09-30 | Add a bunch of reproduction files for bugs. | Xavier Clerc | |
| 2014-09-29 | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau | |
| their eta-expanded forms which can then unfold back to the unfolded primitive projection form. This removes all special code that was necessary to handle primitive projections before, while keeping compatibility. Also fix cbn which was not refolding primitive projections correctly in all cases. Update some test-suite files accordingly. | |||
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau | |
| (but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on. | |||
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | |
| so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections. | |||
| 2014-09-26 | Add a bunch of reproduction files for bugs. | Xavier Clerc | |
| 2014-09-26 | Add missing "Fail" to bug cases. | Xavier Clerc | |
| 2014-09-26 | Bug #3566 is fixed. | Xavier Clerc | |
| 2014-09-25 | Add several reproduction files for bugs. | Xavier Clerc | |
| 2014-09-24 | Update test-suite files. | Matthieu Sozeau | |
| 2014-09-17 | Update test-suite files after last commit. Add a file for rewrite_strat | Matthieu Sozeau | |
| examples. | |||
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau | |
| contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now. | |||
| 2014-09-11 | Fix test-suite files, and move some opened to closed. | Matthieu Sozeau | |
| 2014-09-04 | Status error for bug #3459. | Pierre-Marie Pédrot | |
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau | |
| to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing. | |||
| 2014-08-18 | Fix test-suite file. | Matthieu Sozeau | |
| 2014-08-14 | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | |
| 2014-08-08 | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau | |
| 2014-07-03 | Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵ | Matthieu Sozeau | |
| cleanly when called on partially applied constructors. Also protect evar_conv from that case. | |||
| 2014-07-02 | Indeed simpl never is really honored now. | Matthieu Sozeau | |
| 2014-06-26 | Invalid bug report. | Matthieu Sozeau | |
| 2014-06-26 | Fix bug # 3325 using canonical structure declarations where needed. | Matthieu Sozeau | |
| 2014-06-26 | Add an option to disable typeclass resolution during conversion, which | Matthieu Sozeau | |
| is has non-local effects. For now it is not disabled by default, but we'll try to disable it once the test-suite and contribs are stabilized. | |||
| 2014-06-26 | Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into ↵ | Matthieu Sozeau | |
| JasonGross-tc | |||
| 2014-06-26 | Fixed bug with new semantics of change. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |