aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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-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-20Fix lemma-overloadingMatthieu Sozeau
2015-10-19Do occur-check w.r.t existential's types also when instantiating an evar.Matthieu Sozeau
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
2015-10-18Using appropriate lambda decomposition function counting let-ins whenHugo Herbelin
2015-10-15Avoid 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-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-10-14Occur-check in evar_define was not strong enough.Matthieu Sozeau
2015-10-14Fix constr_matching when a match is found in the head of a case constructMatthieu Sozeau
2015-10-14Fixing evarmap implementation.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Fix rechecking of applications: it can be given ill-typed terms. Fixes math-c...Matthieu Sozeau
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
2015-10-11Fixing obviously untested fold_glob_constr and iter_glob_constr.Hugo Herbelin
2015-10-11Constr_matching: renaming misleading name stk into ctx.Hugo Herbelin
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-10-09Fix inference of return clause raising a type error.Matthieu Sozeau
2015-10-08Univs: fix bug #3807Matthieu Sozeau
2015-10-08Univs: fix bug #4161.Matthieu Sozeau
2015-10-07Univs: fix FingerTree contrib.Matthieu Sozeau
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-06Univs (pretyping): call vm_compute/native_compute with the currentMatthieu Sozeau
2015-10-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau
2015-10-02Univs: fix bug #4251, handling of template polymorphic constants.Matthieu Sozeau
2015-10-02Univs: fix after rebase (from_ctx/from_env)Matthieu Sozeau
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-10-02Univs (pretyping): allow parsing and decl of Top.nMatthieu Sozeau
2015-10-02Univs (evd): deal with global universes and sideffMatthieu Sozeau
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-10-02Univs: force all universes to be >= Set.Matthieu Sozeau
2015-10-02Univs: Fix part of bug #4161Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-27Fixing loss of extra data in Evd.Pierre-Marie Pédrot
2015-09-26Fixing bug #4347: Not_found Exception with some Records.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 20:10:42 +0000