| Commit message (Expand) | Author | Age |
* | Adapting output/Arguments_renaming continued. | Hugo Herbelin | 2014-10-03 |
* | Implement module subtyping for polymorphic constants (errors on | Matthieu Sozeau | 2014-10-02 |
* | Fixing bug #2810 (autounfold on local variable declared as hint but cleared). | Hugo Herbelin | 2014-10-02 |
* | An evar name changed in output test. | Hugo Herbelin | 2014-10-02 |
* | Adapting the output test Notations: | Hugo Herbelin | 2014-10-02 |
* | Added make dependency in %.out in output tests. | Hugo Herbelin | 2014-10-02 |
* | Revert "test-suite: New names for vars but the expected invariant is preserved" | Hugo Herbelin | 2014-10-02 |
* | Adapting output/Arguments_renaming.out after fixing printing of | Hugo Herbelin | 2014-10-02 |
* | Updating to the new use of 3 universes, after Hurkens is simplified. | Hugo Herbelin | 2014-10-01 |
* | Removing test for bug #2080. | Pierre-Marie Pédrot | 2014-10-01 |
* | Add a bunch of reproduction files for closed bugs. | Xavier Clerc | 2014-09-30 |
* | Add a bunch of reproduction files for bugs. | Xavier Clerc | 2014-09-30 |
* | Seeing IntroWildcard as an action intro pattern rather than as a naming pattern | Hugo Herbelin | 2014-09-30 |
* | Restoring non-uniform delta on local and global constants in 2nd order | Hugo Herbelin | 2014-09-29 |
* | Adding a test for bug #2428. | Pierre-Marie Pédrot | 2014-09-29 |
* | Bug fixed. | Matthieu Sozeau | 2014-09-29 |
* | Fix test-suite files | Matthieu Sozeau | 2014-09-29 |
* | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau | 2014-09-29 |
* | Keyed unification option, compiling the whole standard library | Matthieu Sozeau | 2014-09-27 |
* | First version of keyed subterm selection in unification. | Matthieu Sozeau | 2014-09-27 |
* | Fix test-suite file. | Matthieu Sozeau | 2014-09-27 |
* | Fix bug #3664 by refolding projections that don't reduce in cbn. | Matthieu Sozeau | 2014-09-27 |
* | Fix semantics of matching with folded/unfolded projections to definitely | Matthieu Sozeau | 2014-09-27 |
* | Fix bug #3672, application of primitive projections as coercions. | Matthieu Sozeau | 2014-09-27 |
* | Fix bug 3662 by actually reducing primitive projections in cbv/compute. | Matthieu Sozeau | 2014-09-27 |
* | Bug fixed. | Matthieu Sozeau | 2014-09-27 |
* | Make pattern_of_constr typed so that we can infer the proper patterns | Matthieu Sozeau | 2014-09-27 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Adapting to naming of evars. | Hugo Herbelin | 2014-09-27 |
* | Fix canonical structure resolution which was launched on the results of | Matthieu Sozeau | 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-26 |
* | Adding a test for bug #3653. | Pierre-Marie Pédrot | 2014-09-26 |
* | Test cases for closed bugs. | Xavier Clerc | 2014-09-26 |
* | Add several reproduction files for bugs. | Xavier Clerc | 2014-09-25 |
* | Update test-suite files. | Matthieu Sozeau | 2014-09-24 |
* | Fix bug #3656. | Matthieu Sozeau | 2014-09-23 |
* | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau | 2014-09-19 |
* | Fixing #3641 (loop in e_contextually, introduced in r16525). | Hugo Herbelin | 2014-09-19 |
* | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau | 2014-09-18 |
* | Fix debug printing with primitive projections. | Matthieu Sozeau | 2014-09-18 |
* | Reductionops: (Co)Fixpoints are always refolded during iota | Pierre Boutillier | 2014-09-18 |
* | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau | 2014-09-17 |
* | Fix bug #3633 properly, by delaying the interpetation of constrs in | Matthieu Sozeau | 2014-09-17 |
* | Revert "While resolving typeclass evars in clenv, touch only the ones that ap... | Matthieu Sozeau | 2014-09-17 |
* | While resolving typeclass evars in clenv, touch only the ones that appear in the | Matthieu Sozeau | 2014-09-17 |
* | Update test-suite files after last commit. Add a file for rewrite_strat | Matthieu Sozeau | 2014-09-17 |
* | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau | 2014-09-17 |
* | Undo prints only if coqtop || emacs | Enrico Tassi | 2014-09-16 |