| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-06-26 | Deactivate the "Standard Propositions Naming" flag, source of a lot of | Hugo Herbelin |
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau |
| 2014-06-04 | Make standard library independent of the names generated by | Hugo Herbelin |
| 2014-06-04 | Make standard library independent of the names generated by | Hugo Herbelin |
| 2014-06-04 | Small lemma about Relations. | Hugo Herbelin |
| 2014-06-04 | Remove spurious Show in script. | Matthieu Sozeau |
| 2014-06-01 | Making those proofs which depend on names generated for the arguments | Hugo Herbelin |
| 2014-05-31 | Basic lemmas about the algebraic structure of equality. | Hugo Herbelin |
| 2014-05-26 | Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q | Pierre Boutillier |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-20 | Moving (e)transitivity out of the AST. | Pierre-Marie Pédrot |
| 2014-05-18 | Revert "Fix Qcanon after changes on injection." | Maxime Dénès |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-05-09 | Update and start testing rewrite-in-type code. | Matthieu Sozeau |
| 2014-05-09 | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau |
| 2014-05-07 | Removing comment outdated since eta holds in conversion rule (this | Hugo Herbelin |
