| Age | Commit message (Expand) | Author |
|---|
| 2014-07-22 | Revert "Propagate size info through pattern matching in predicates, for the" | Maxime Dénès |
| 2014-07-22 | Propagate size info through pattern matching in predicates, for the | Maxime Dénès |
| 2014-07-22 | Extend subterm relation to pattern matching in return predicates. | Maxime Dénès |
| 2014-07-22 | Fix check_inductive_codomain. | Maxime Dénès |
| 2014-07-22 | Refine check_is_subterm. | Maxime Dénès |
| 2014-07-22 | Refined guard condition of cofixpoints, to anticipate potential futur | Maxime Dénès |
| 2014-07-22 | First attempt at a fix for guard condition on cofixpoints. | Maxime Dénès |
| 2014-07-22 | Add test-suite file for guard condition on cofixpoints. | Maxime Dénès |
| 2014-07-22 | Typo in comment. | Maxime Dénès |
| 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-22 | Made intersection on regular trees less intensional. | Maxime Dénès |
| 2014-07-22 | Refining match subterm and commutative cut rules. The parameters that are | Maxime Dénès |
| 2014-07-22 | Tentative fix for the commutative cut subterm rule. | Maxime Dénès |
| 2014-07-22 | Tentative patch for incompatibility between subterm relation and dependent | Maxime Dénès |
| 2014-07-22 | Ide: Drop argument added by MacOS during .app launch | Pierre Boutillier |
| 2014-07-22 | the art of forgetting new files during rebase -i | Pierre Boutillier |
| 2014-07-22 | A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundle | Pierre Boutillier |
| 2014-07-22 | Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file exists | Pierre Boutillier |
| 2014-07-22 | When I make MacOS binary, I would like to have a coqtop able to speak to coqi... | Pierre Boutillier |
| 2014-07-22 | Small code sharing in TacticMatching. | Pierre-Marie Pédrot |
| 2014-07-22 | Adding a "is_val" primitive to IStream. | Pierre-Marie Pédrot |
| 2014-07-21 | Universe level maps use HMaps. | Pierre-Marie Pédrot |
| 2014-07-21 | Missing primitives in HMap. | Pierre-Marie Pédrot |
| 2014-07-21 | Fixing semantics of HSet.inter and HSet.diff. | Pierre-Marie Pédrot |
| 2014-07-21 | More straightforward definition of Universes.add_list_map. | Pierre-Marie Pédrot |
| 2014-07-21 | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau |
| 2014-07-21 | Fixing output test-suite. | Pierre-Marie Pédrot |
| 2014-07-21 | Correct eauto which was not dealing properly with polymorphic constants. | Matthieu Sozeau |
| 2014-07-21 | Cleanup code for constant equality in kernel conversion. | Matthieu Sozeau |
| 2014-07-21 | Missing space in pretty-printer | Pierre-Marie Pédrot |
| 2014-07-21 | Documenting the changes of Locate semantics. | Pierre-Marie Pédrot |
| 2014-07-21 | Unifying locate code, also making it more powerful: it is now able to find | Pierre-Marie Pédrot |
| 2014-07-21 | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot |
| 2014-07-21 | More complete printing of Ltac location, akin to the term-dedicated Locate co... | Pierre-Marie Pédrot |
| 2014-07-21 | Documenting the need of the "DECLARE PLUGIN" statement. | Pierre-Marie Pédrot |
| 2014-07-21 | Documenting the change of semantics of the "constructor" tactic. | Pierre-Marie Pédrot |
| 2014-07-21 | Adding a test-suite for bug #3422. | Pierre-Marie Pédrot |
| 2014-07-20 | Use kernel conversion on terms that contain universe variables during unifica... | Matthieu Sozeau |
| 2014-07-17 | Fix coercion code to disallow using cumulativity in the domain of products, w... | Matthieu Sozeau |
| 2014-07-17 | Completing c236b51348d2 by fixing EqdepFactsv actually committing the | Hugo Herbelin |
| 2014-07-16 | Adding a test-suite for bug #3416. | Pierre-Marie Pédrot |
| 2014-07-16 | Fixing universe substitution in mutual fixpoints. | Pierre-Marie Pédrot |
| 2014-07-16 | STM: check-vi-task fixed | Enrico Tassi |
| 2014-07-16 | STM: Goal printing got wrong in a merge, fixed | Enrico Tassi |
| 2014-07-16 | - Fix bug introduced in obligations which wouldn't consider all evars that are | Matthieu Sozeau |
| 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-15 | Using the generic timeout function in the boostrapped file. | Pierre-Marie Pédrot |
