aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2015-09-18Do not compress match constructs when the inner match contains no branch. (Fi...Guillaume Melquiond
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-09-08Documenting the code when preference is given to expansion of defaultHugo Herbelin
2015-08-02Continuing 817308ab (use ltac env for terms in ltac context) + fixHugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Documenting in passing.Hugo Herbelin
2015-08-02Hopefully clearer printing of stack when debugging evarconv unification.Hugo Herbelin
2015-08-02Cosmetic changes in evarconv.ml: hopefully more regular names and formHugo Herbelin
2015-08-02Cosmetic changes in evarconv.ml: hopefully more regular form andHugo Herbelin
2015-08-02Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Hugo Herbelin
2015-08-02Evarconv.ml: small cut-elimination, saving useless zip.Hugo Herbelin
2015-08-02Cosmetic in evarconv.ml: naming a local function for better readibility.Hugo Herbelin
2015-08-02Fixing #4221 (interpreting bound variables using ltac env was possiblyHugo Herbelin
2015-07-21Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2015-07-16Refining 71def2f8 on too strong occur-check limiting evar-evarHugo Herbelin
2015-07-16Slight improvement in naming anonymous variables in error messages:Hugo Herbelin
2015-07-16Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Hugo Herbelin
2015-07-16Fixing bug #4240 (closure_of_filter was not ensuring refinement ofHugo Herbelin
2015-07-16Fix universe instantiation with canonical structures.Maxime Dénès
2015-07-16Continuing 93579407, spotting other potential sources of anomalyHugo Herbelin
2015-07-16Fixing anomaly #3743 while printing an error message involving evar constraints.Hugo Herbelin
2015-07-10Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.Hugo Herbelin
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-09Make retyping of projections more resilient to wrong environment.Maxime Dénès
2015-07-07Univs: bug fix.Matthieu Sozeau
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-06-28Fix incompleteness of conversion used by evarconvMatthieu Sozeau
2015-06-26Fix bug #4254 with the help of J.H. JourdanMatthieu Sozeau
2015-06-08Make normalization of primitive projections in native_compute the same as wit...Maxime Dénès
2015-05-28Fixup for 866c41bEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 17:07:46 +0000