aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Use the canonical name when looking for an eliminator (bug #4670).Gravatar Guillaume Melquiond2016-05-03
* Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Gravatar Guillaume Melquiond2016-05-02
* Fix incorrect cbv reduction of primitive projections. (Bug #4634)Gravatar Guillaume Melquiond2016-04-29
* Optimization in building a return clause by pattern-matching: do notGravatar Hugo Herbelin2016-04-27
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* Fix a bug in Program coercion codeGravatar Matthieu Sozeau2016-03-25
* Fix #4623: set tactic too weak with universes (regression)Gravatar Maxime Dénès2016-03-17
* Fix incorrect behavior of CS resolutionGravatar Matthieu Sozeau2016-03-16
* Try eta-expansion of records only on non-recursive onesGravatar Matthieu Sozeau2016-03-15
* Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* Fix strategy of Keyed UnificationGravatar Matthieu Sozeau2016-03-09
* Fix part of bug #4533: respect declared global transparency ofGravatar Matthieu Sozeau2016-02-23
* Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* Optimizing the computation of frozen evars.Gravatar Pierre-Marie Pédrot2016-02-03
* Opacifying the type of evar naming structure in Evd.Gravatar Pierre-Marie Pédrot2016-02-03
* More compact representation for evar resolvability flag.Gravatar Pierre-Marie Pédrot2016-02-03
* Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Gravatar Pierre-Marie Pédrot2016-01-27
* Fix bug #4519: oops, global shadowed local universe level bindings.Gravatar Matthieu Sozeau2016-01-23
* Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formGravatar Matthieu Sozeau2016-01-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
* Extend last commit: keyed unification uses full conversions on the applied co...Gravatar Matthieu Sozeau2016-01-12
* Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Gravatar Pierre-Marie Pédrot2015-12-29
* (Partial) fix for bug #4453: raise an error instead of an anomaly.Gravatar Matthieu Sozeau2015-12-17
* Optimize occur_evar_upto_types, avoiding repeateadly looking into theGravatar Matthieu Sozeau2015-12-11
* Add an option to deactivate compatibility printing of primitiveGravatar Matthieu Sozeau2015-12-02
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).Gravatar Hugo Herbelin2015-11-25
* Fixing an old typo in Retyping, found by Matej.Gravatar Hugo Herbelin2015-11-24
* Fixing a vm_compute bug in the presence of let-ins among theGravatar Hugo Herbelin2015-11-22
* Fixing a bug of adjust_subst_to_rel_context.Gravatar Hugo Herbelin2015-11-22
* Fixing kernel bug in typing match with let-ins in the arity.Gravatar Hugo Herbelin2015-11-22
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
* Ensure that conversion is called on terms of the same type inGravatar Matthieu Sozeau2015-11-11
* Fix bug #3998: when using typeclass resolution for conversion, allowGravatar Matthieu Sozeau2015-11-11
* Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
* Pushing the backtrace in conversion anomalies.Gravatar Pierre-Marie Pédrot2015-11-09
* Univs: missing checks in evarsolve with candidates and missing aGravatar Matthieu Sozeau2015-11-04
* Univs: update refman, better printers for universe contexts.Gravatar Matthieu Sozeau2015-11-04
* Univs: compatibility with 8.4.Gravatar Matthieu Sozeau2015-11-04
* Fix bug #4151: discrepancy between exact and eexact/eassumption.Gravatar Matthieu Sozeau2015-11-02
* Refresh rigid universes as well, and in 8.4 compatibility mode,Gravatar Matthieu Sozeau2015-11-02
* Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Fix bug in native compiler with universe polymorphism.Gravatar Maxime Dénès2015-10-28
* Refine Gregory Malecha's patch on VM and universe polymorphism.Gravatar Maxime Dénès2015-10-28
* Conversion of polymorphic inductive types was incomplete in VM and native.Gravatar Maxime Dénès2015-10-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:30:56 +0000