aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"Gravatar Hugo Herbelin2015-10-28
* Documenting a bit more interpretation functions in passing.Gravatar Hugo Herbelin2015-10-26
* Fix lemma-overloadingGravatar Matthieu Sozeau2015-10-20
* Do occur-check w.r.t existential's types also when instantiating an evar.Gravatar Matthieu Sozeau2015-10-19
* Using "__" rather than this unelegant arbitrary "A" for the name of variables...Gravatar Hugo Herbelin2015-10-18
* Fixing #4198 (continued): not matching within the inner lambdas/let-insGravatar Hugo Herbelin2015-10-18
* Using appropriate lambda decomposition function counting let-ins whenGravatar Hugo Herbelin2015-10-18
* Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
* Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Occur-check in evar_define was not strong enough.Gravatar Matthieu Sozeau2015-10-14
* Fix constr_matching when a match is found in the head of a case constructGravatar Matthieu Sozeau2015-10-14
* Fixing evarmap implementation.Gravatar Pierre-Marie Pédrot2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Fix rechecking of applications: it can be given ill-typed terms. Fixes math-c...Gravatar Matthieu Sozeau2015-10-12
* Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* Refining 0c320e79ba30 in fixing interpretation of constr under bindersGravatar Hugo Herbelin2015-10-11
* Fixing obviously untested fold_glob_constr and iter_glob_constr.Gravatar Hugo Herbelin2015-10-11
* Constr_matching: renaming misleading name stk into ctx.Gravatar Hugo Herbelin2015-10-11
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* Fix inference of return clause raising a type error.Gravatar Matthieu Sozeau2015-10-09
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* Univs: fix bug #4161.Gravatar Matthieu Sozeau2015-10-08
* Univs: fix FingerTree contrib.Gravatar Matthieu Sozeau2015-10-07
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Univs (pretyping): call vm_compute/native_compute with the currentGravatar Matthieu Sozeau2015-10-06
* Fix bug #4354: interpret hints in the right env and sigma.Gravatar Matthieu Sozeau2015-10-06
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Univs (pretyping): allow parsing and decl of Top.nGravatar Matthieu Sozeau2015-10-02
* Univs (evd): deal with global universes and sideffGravatar Matthieu Sozeau2015-10-02
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* Univs: force all universes to be >= Set.Gravatar Matthieu Sozeau2015-10-02
* Univs: Fix part of bug #4161Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Fixing loss of extra data in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
* Fixing bug #4347: Not_found Exception with some Records.Gravatar Pierre-Marie Pédrot2015-09-26
* Do not compress match constructs when the inner match contains no branch. (Fi...Gravatar Guillaume Melquiond2015-09-18
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Documenting the code when preference is given to expansion of defaultGravatar Hugo Herbelin2015-09-08
* Continuing 817308ab (use ltac env for terms in ltac context) + fixGravatar Hugo Herbelin2015-08-02
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Documenting in passing.Gravatar Hugo Herbelin2015-08-02
* Hopefully clearer printing of stack when debugging evarconv unification.Gravatar Hugo Herbelin2015-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 20:45:30 +0000