| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-07-17 | Completing c236b51348d2 by fixing EqdepFactsv actually committing the | Hugo Herbelin |
| 2014-07-15 | Added a (constructive) proof of Weak Konig's lemma for decidable trees. | Hugo Herbelin |
| 2014-07-15 | Some basics facts about eq_dep. | Hugo Herbelin |
| 2014-07-10 | MSetRBT: unfortunate typo in compare_height (fix #3413) | Pierre Letouzey |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2014-07-08 | Fixing bug #3270. Patch by Robbert Krebbers. | Pierre-Marie Pédrot |
| 2014-06-29 | Move Params definition in generalize rewriting out of a section so that | Matthieu Sozeau |
| 2014-06-26 | Avoid using a deprecated lemma in the standard library. | Guillaume Melquiond |
| 2014-06-26 | Remove some theories that have been deprecated for 10 years. | Guillaume Melquiond |
| 2014-06-26 | Export the right modules in Setoid, avoiding anomalies in generalized rewriting. | Matthieu Sozeau |
