| Age | Commit message (Expand) | Author |
|---|
| 2014-10-27 | Fix some typos in comments. | Guillaume Melquiond |
| 2014-10-22 | EqdepFacts: generalize statements which were wrongly restricted to Prop. | Arnaud Spiwack |
| 2014-10-22 | Fixing typo absorption (bug #3751). | Hugo Herbelin |
| 2014-10-17 | Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq... | Hugo Herbelin |
| 2014-10-17 | Essai où assert_style n'est utilisé que si pas visuellement une équation; | Hugo Herbelin |
| 2014-10-16 | ConstructiveEpsilon: simplify the before_witness type using non-uniform param... | Arnaud Spiwack |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-10-10 | Give the same argument name for the record binder of type class | Matthieu Sozeau |
| 2014-10-10 | Fix segfault in native compiler on int31 division. | Maxime Dénès |
| 2014-10-01 | eta contractions | Pierre Boutillier |
| 2014-10-01 | argument flip of Cyclic31.nshiftr and Cyclic31.nshiftl | Pierre Boutillier |
| 2014-10-01 | Simpl less (so that cbn will not simpl too much) | Pierre Boutillier |
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau |
| 2014-09-26 | Hurkens.v: Fix a syntax error. | Arnaud Spiwack |
| 2014-09-26 | ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr... | Arnaud Spiwack |
| 2014-09-26 | Hurkens.v: new paradox: type of modal propositions is not a retract. | Arnaud Spiwack |
| 2014-09-26 | Hurkens.v: fix coqdoc formatting in a comment. | Arnaud Spiwack |
| 2014-09-25 | Hurkens.v: update comments. | Arnaud Spiwack |
| 2014-09-24 | Return a Prop not an arbitrary Type, and correct a typo. | Matthieu Sozeau |
| 2014-09-24 | Hurkens.v: show proofs in coqdoc. | Arnaud Spiwack |
| 2014-09-24 | Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}]. | Arnaud Spiwack |
| 2014-09-24 | Hurkens.v: coqdoc documentation. | Arnaud Spiwack |
| 2014-09-24 | A new version of Hurkens.v. | Arnaud Spiwack |
| 2014-09-23 | adds general facts in the Reals library, whose need was detected in | Yves Bertot |
| 2014-09-17 | Change some Defined into Qed. | Guillaume Melquiond |
| 2014-09-17 | Add some missing Proof statements. | Guillaume Melquiond |
| 2014-09-17 | Change an axiom into a definition. | Guillaume Melquiond |
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau |
| 2014-09-08 | Removing the XML plugin. | Pierre-Marie Pédrot |
| 2014-08-26 | Prove forall extensionality | Jason Gross |
| 2014-08-26 | sed s'/_one_var/_on/g' | Jason Gross |
| 2014-08-26 | Generalize EqdepFacts | Jason Gross |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross |
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin |
| 2014-08-18 | Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to | Hugo Herbelin |
| 2014-08-12 | A couple of fixes/improvements in -beautify, but backtracking on | Hugo Herbelin |
| 2014-08-07 | Instead of relying on a trick to make the constructor tactic parse, put | Pierre-Marie Pédrot |
| 2014-08-07 | Removing the "constructor" tactic from the AST. | Pierre-Marie Pédrot |
| 2014-08-05 | Improving printing of "[]" (nil) in spite of the risk of collision | Hugo Herbelin |
| 2014-08-05 | Testing beautifying on an example. | Hugo Herbelin |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | Testing a replacement of "cut" by "enough" on a couple of test files. | Hugo Herbelin |
| 2014-08-05 | More proofs independent of the names generated by induction/elim over | Hugo Herbelin |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-31 | Adding a generalized version of fold_Equal to FMapFacts. | Pierre Courtieu |
| 2014-07-22 | Simplified rect2, it turns out Arthur's trick was not required. | Maxime Dénès |
| 2014-07-22 | A version of Fin.rect2 that is compatible with the fix of the guard condition. | Maxime Dénès |
| 2014-07-22 | Fixed proof of irrelevance of le on nat, inspired by the | Maxime Dénès |
