| Commit message (Expand) | Author | Age |
* | Do not give a name to anonymous evars anymore. See bug #4547. | Pierre-Marie Pédrot | 2016-02-13 |
* | 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-02-03 |
* | Fix bug #4537: Coq 8.5 is slower in typeclass resolution. | Pierre-Marie Pédrot | 2016-01-27 |
* | 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-23 |
* | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | 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 | 2016-01-12 |
* | Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found. | Pierre-Marie Pédrot | 2015-12-29 |
* | (Partial) fix for bug #4453: raise an error instead of an anomaly. | Matthieu Sozeau | 2015-12-17 |
* | Optimize occur_evar_upto_types, avoiding repeateadly looking into the | Matthieu Sozeau | 2015-12-11 |
* | Add an option to deactivate compatibility printing of primitive | Matthieu Sozeau | 2015-12-02 |
* | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau | 2015-11-27 |
* | Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej). | Hugo Herbelin | 2015-11-25 |
* | Fixing an old typo in Retyping, found by Matej. | Hugo Herbelin | 2015-11-24 |
* | 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-22 |
* | Fix bug #4433, removing hack on evars appearing in a pattern from a | Matthieu Sozeau | 2015-11-19 |
* | Performance fix for destruct. | Pierre-Marie Pédrot | 2015-11-17 |
* | 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-11 |
* | Pushing the backtrace in conversion anomalies. | Pierre-Marie Pédrot | 2015-11-09 |
* | 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-04 |
* | 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-11-02 |
* | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau | 2015-10-29 |
* | 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-28 |
* | Documenting a bit more interpretation functions in passing. | Hugo Herbelin | 2015-10-26 |
* | Fix lemma-overloading | Matthieu Sozeau | 2015-10-20 |
* | Do occur-check w.r.t existential's types also when instantiating an evar. | Matthieu Sozeau | 2015-10-19 |
* | Using "__" rather than this unelegant arbitrary "A" for the name of variables... | Hugo Herbelin | 2015-10-18 |
* | Fixing #4198 (continued): not matching within the inner lambdas/let-ins | Hugo Herbelin | 2015-10-18 |
* | Using appropriate lambda decomposition function counting let-ins when | Hugo Herbelin | 2015-10-18 |
* | Avoid dependency of the pretyper on C code. | Maxime Dénès | 2015-10-15 |
* | Fix #4346 2/2: VM casts were not inferring universe constraints. | Maxime Dénès | 2015-10-15 |
* | Fix #4346 1/2: native casts were not inferring universe constraints. | Maxime Dénès | 2015-10-15 |
* | Occur-check in evar_define was not strong enough. | Matthieu Sozeau | 2015-10-14 |