aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
* Cosmetic changes in evarconv.ml: hopefully more regular names and formGravatar Hugo Herbelin2015-08-02
* Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
* Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
* Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
* Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
* Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
* Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2015-07-21
* Refining 71def2f8 on too strong occur-check limiting evar-evarGravatar Hugo Herbelin2015-07-16
* Slight improvement in naming anonymous variables in error messages:Gravatar Hugo Herbelin2015-07-16
* Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Gravatar Hugo Herbelin2015-07-16
* Fixing bug #4240 (closure_of_filter was not ensuring refinement ofGravatar Hugo Herbelin2015-07-16
* Fix universe instantiation with canonical structures.Gravatar Maxime Dénès2015-07-16
* Continuing 93579407, spotting other potential sources of anomalyGravatar Hugo Herbelin2015-07-16
* Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
* Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.Gravatar Hugo Herbelin2015-07-10
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* Make retyping of projections more resilient to wrong environment.Gravatar Maxime Dénès2015-07-09
* Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 02:44:23 +0000