| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-06-26 | Duplicate | Matthieu Sozeau | |
| 2014-06-26 | This has been fixed. | Matthieu Sozeau | |
| 2014-06-26 | Properly refresh the local hintdb database in case an external tactic changed | Matthieu Sozeau | |
| the hypotheses in eauto. | |||
| 2014-06-26 | Fix test-suite file, adding the proper Fail. | Matthieu Sozeau | |
| 2014-06-26 | Bug #3329 is closed. | Matthieu Sozeau | |
| 2014-06-26 | 3392 is now closed thanks to E. Tassi. | Matthieu Sozeau | |
| 2014-06-26 | Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into ↵ | Matthieu Sozeau | |
| JasonGross-more-test-suite Conflicts: test-suite/bugs/closed/3300.v test-suite/bugs/closed/3373.v | |||
| 2014-06-26 | Fix test-suite files. | Matthieu Sozeau | |
| 2014-06-26 | Bug #3301 is closed, the projection cannot be defined anymore. | Matthieu Sozeau | |
| 2014-06-26 | Fix test-suite file for opened bug #1596 | Matthieu Sozeau | |
| 2014-06-24 | Update some bugs about typeclass resolution | Jason Gross | |
| 2014-06-23 | Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344) | Enrico Tassi | |
| Every time you use abstract a kitten dies, please stop. | |||
| 2014-06-22 | More test-suite cases | Jason Gross | |
| 2014-06-21 | - Add an option to refresh only algebraic universes, for e_type_of. The goal | Matthieu Sozeau | |
| there is not the same as in Evd.define. - Fixed bugs #3330 and #3331. | |||
| 2014-06-20 | Fixed bug 3332. | Matthieu Sozeau | |
| 2014-06-20 | Allow more relaxed conversion between the types of the two terms of a rewrite | Matthieu Sozeau | |
| equation, fix uncaught exception in setoid_rewrite (bug #3336). | |||
| 2014-06-20 | Fix computation of inductive level in monomorphism + indices-matter mode. | Matthieu Sozeau | |
| Fixes bug #3346. | |||
| 2014-06-20 | Fixed some HoTT bugs, provide a proper error message when giving an ill-formed | Matthieu Sozeau | |
| universe instance. | |||
| 2014-06-20 | Bug 27 closed now that universe contexts can be refined during the proof, | Matthieu Sozeau | |
| here instantiating a flexible level with Set. | |||
| 2014-06-19 | HoTT coq bug #62 fixed. | Matthieu Sozeau | |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | |
| and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup. | |||
| 2014-06-17 | Fix a destArity that does not exactly match isArity in presence of let-ins. | Matthieu Sozeau | |
| 2014-06-17 | Reinstate eta for records in evarconv, fixing two HoTT coq bugs. | Matthieu Sozeau | |
| 2014-06-17 | Not a bug, keep for backwards compatibility | Matthieu Sozeau | |
| 2014-06-17 | Bug closed, now in polymorphic mode, Variables A B : Type give different ↵ | Matthieu Sozeau | |
| levels to A and B. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |