aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
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
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-15Merge branch 'v8.5'Pierre-Marie Pédrot
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
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-29Ensuring more invariants in Constr_matching.Pierre-Marie Pédrot
2015-03-29Fixing bug #4165.Pierre-Marie Pédrot
2015-03-27use a more compact representation of non-constant constructorsBenjamin Gregoire
2015-03-26Fix bug 4157,Benjamin Gregoire
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
2015-03-25Use kernel names instead of user names when looking for coercions. (Fix for b...Guillaume Melquiond
2015-03-24Fixing equality of notation_constrs. Fixes bug #4136.Pierre-Marie Pédrot
2015-03-17Add function to fix the non-substituted universe variables of an evar_map.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 12:15:10 +0000