aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2015-09-09Merge remote-tracking branch 'origin/v8.5' into trunkHugo Herbelin
2015-09-08Documenting the code when preference is given to expansion of defaultHugo Herbelin
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
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-27Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-21Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2015-07-18Merge branch 'v8.5'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-06Merge branch 'v8.5' into trunkMaxime Dénès
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-28Merge branch 'v8.5'Pierre-Marie Pédrot
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-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-08Make normalization of primitive projections in native_compute the same as wit...Maxime Dénès
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
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-15Merge v8.5 into trunkHugo Herbelin
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-05-05Merge branch 'v8.5'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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-10 02:29:37 +0000