aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-19Adding an extensible global state to evarmaps.Pierre-Marie Pédrot
2015-05-15Make Coercion.inh_app_fun respect its specification.Pierre-Marie Pédrot
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-05-13Fix for a second avatar of bug #4234.Pierre-Marie Pédrot
2015-05-13Better fixing #4198 such that the term to match is looked for beforeHugo Herbelin
2015-05-12Fixing bug #4234.Pierre-Marie Pédrot
2015-05-10Code factorization in Constr_matching.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-22Fixing non exhaustive pattern-matching.Hugo Herbelin
2015-04-21Fixing #4198 (looking for subterms also in the return clause of match).Hugo Herbelin
2015-04-21Fixing #3383 (a "return" clause without an "in" clause is not enoughHugo Herbelin
2015-04-21Some dead code.Hugo Herbelin
2015-04-09Really fix constr_of_pattern and bugs #3590 and #4120 byMatthieu Sozeau
2015-04-09Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic...Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 11:20:29 +0000