| Age | Commit message (Expand) | Author |
|---|
| 2016-04-19 | Fixing #4677 (collision of a global variable and of a local variable | Hugo Herbelin |
| 2016-03-25 | Fix a bug in Program coercion code | Matthieu Sozeau |
| 2016-03-17 | Fix #4623: set tactic too weak with universes (regression) | Maxime Dénès |
| 2016-03-16 | Fix incorrect behavior of CS resolution | Matthieu Sozeau |
| 2016-03-15 | Try eta-expansion of records only on non-recursive ones | Matthieu Sozeau |
| 2016-03-10 | Primitive projections: protect kernel from erroneous definitions. | Matthieu Sozeau |
| 2016-03-09 | Fix strategy of Keyed Unification | Matthieu Sozeau |
| 2016-02-23 | Fix part of bug #4533: respect declared global transparency of | Matthieu Sozeau |
| 2016-02-13 | Do not give a name to anonymous evars anymore. See bug #4547. | Pierre-Marie Pédrot |
| 2016-02-03 | Optimizing the computation of frozen evars. | Pierre-Marie Pédrot |
| 2016-02-03 | Opacifying the type of evar naming structure in Evd. | Pierre-Marie Pédrot |
| 2016-02-03 | More compact representation for evar resolvability flag. | Pierre-Marie Pédrot |
| 2016-01-27 | Fix bug #4537: Coq 8.5 is slower in typeclass resolution. | Pierre-Marie Pédrot |
| 2016-01-23 | Fix bug #4519: oops, global shadowed local universe level bindings. | Matthieu Sozeau |
| 2016-01-23 | Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form | Matthieu Sozeau |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-12 | Fixing #4256 and #4484 (changes in evar-evar resolution made that new | Hugo Herbelin |
| 2016-01-12 | Extend last commit: keyed unification uses full conversions on the applied co... | Matthieu Sozeau |
| 2016-01-12 | Fix essential bug in new Keyed Unification mode reported by R. Krebbers. | Matthieu Sozeau |
| 2015-12-29 | Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found. | Pierre-Marie Pédrot |
| 2015-12-17 | (Partial) fix for bug #4453: raise an error instead of an anomaly. | Matthieu Sozeau |
| 2015-12-11 | Optimize occur_evar_upto_types, avoiding repeateadly looking into the | Matthieu Sozeau |
| 2015-12-02 | Add an option to deactivate compatibility printing of primitive | Matthieu Sozeau |
| 2015-11-27 | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau |
| 2015-11-25 | Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej). | Hugo Herbelin |
| 2015-11-24 | Fixing an old typo in Retyping, found by Matej. | Hugo Herbelin |
| 2015-11-22 | Fixing a vm_compute bug in the presence of let-ins among the | Hugo Herbelin |
| 2015-11-22 | Fixing a bug of adjust_subst_to_rel_context. | Hugo Herbelin |
| 2015-11-22 | Fixing kernel bug in typing match with let-ins in the arity. | Hugo Herbelin |
| 2015-11-19 | Fix bug #4433, removing hack on evars appearing in a pattern from a | Matthieu Sozeau |
| 2015-11-17 | Performance fix for destruct. | Pierre-Marie Pédrot |
| 2015-11-11 | Ensure that conversion is called on terms of the same type in | Matthieu Sozeau |
| 2015-11-11 | Fix bug #3998: when using typeclass resolution for conversion, allow | Matthieu Sozeau |
| 2015-11-11 | Fix bug #4293: ensure let-ins do not contain algebraic universes in | Matthieu Sozeau |
| 2015-11-09 | Pushing the backtrace in conversion anomalies. | Pierre-Marie Pédrot |
| 2015-11-04 | Univs: missing checks in evarsolve with candidates and missing a | Matthieu Sozeau |
| 2015-11-04 | Univs: update refman, better printers for universe contexts. | Matthieu Sozeau |
| 2015-11-04 | Univs: compatibility with 8.4. | Matthieu Sozeau |
| 2015-11-02 | Fix bug #4151: discrepancy between exact and eexact/eassumption. | Matthieu Sozeau |
| 2015-11-02 | Refresh rigid universes as well, and in 8.4 compatibility mode, | Matthieu Sozeau |
| 2015-10-29 | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau |
| 2015-10-28 | Univs: local names handling. | Matthieu Sozeau |
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi |
| 2015-10-28 | Fix bug in native compiler with universe polymorphism. | Maxime Dénès |
| 2015-10-28 | Refine Gregory Malecha's patch on VM and universe polymorphism. | Maxime Dénès |
| 2015-10-28 | Conversion of polymorphic inductive types was incomplete in VM and native. | Maxime Dénès |
| 2015-10-28 | Adds support for the virtual machine to perform reduction of universe polymor... | Gregory Malecha |
| 2015-10-28 | Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" | Hugo Herbelin |
| 2015-10-26 | Documenting a bit more interpretation functions in passing. | Hugo Herbelin |
| 2015-10-20 | Fix lemma-overloading | Matthieu Sozeau |
