aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2015-12-05An example in centralizing similar functions to a common place so thatHugo Herbelin
2015-12-04Removing dynamic inclusion of constrs in tactic AST.Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Add an option to deactivate compatibility printing of primitiveMatthieu Sozeau
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-26More efficient implementation of equality-up-to-universes in Universes.Pierre-Marie Pédrot
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-25Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).Hugo Herbelin
2015-11-24Fixing an old typo in Retyping, found by Matej.Hugo Herbelin
2015-11-22Fixing a vm_compute bug in the presence of let-ins among theHugo Herbelin
2015-11-22Fixing a bug of adjust_subst_to_rel_context.Hugo Herbelin
2015-11-22Fixing kernel bug in typing match with let-ins in the arity.Hugo Herbelin
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-11Ensure that conversion is called on terms of the same type inMatthieu Sozeau
2015-11-11Fix bug #3998: when using typeclass resolution for conversion, allowMatthieu Sozeau
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
2015-11-10Revert "Fixing #1225: we now skip the canonically built binding contexts of"Hugo Herbelin
2015-11-10Fixing #1225: we now skip the canonically built binding contexts ofHugo Herbelin
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
2015-11-09Pushing the backtrace in conversion anomalies.Pierre-Marie Pédrot
2015-11-07Experimenting printing the type of the defined term of a LetIn whenHugo Herbelin
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Univs: missing checks in evarsolve with candidates and missing aMatthieu Sozeau
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-11-04Univs: compatibility with 8.4.Matthieu Sozeau
2015-11-02Fix bug #4151: discrepancy between exact and eexact/eassumption.Matthieu Sozeau
2015-11-02Refresh rigid universes as well, and in 8.4 compatibility mode,Matthieu Sozeau
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
2015-10-29Removing some goal unsafeness in inductive schemes.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28Fix bug in native compiler with universe polymorphism.Maxime Dénès
2015-10-28Refine Gregory Malecha's patch on VM and universe polymorphism.Maxime Dénès
2015-10-28Conversion of polymorphic inductive types was incomplete in VM and native.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-28Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"Hugo Herbelin
2015-10-26Documenting a bit more interpretation functions in passing.Hugo Herbelin
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-20Fix lemma-overloadingMatthieu Sozeau
2015-10-19Do occur-check w.r.t existential's types also when instantiating an evar.Matthieu Sozeau
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19More monotonicity in Tactics.Pierre-Marie Pédrot
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-10-18Using "__" rather than this unelegant arbitrary "A" for the name of variables...Hugo Herbelin
2015-10-18Fixing #4198 (continued): not matching within the inner lambdas/let-insHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 08:21:26 +0000