aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-02 19:39:34 +0000