aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2016-06-15Allow `Pretyping.search_guard` to not check guardArnaud Spiwack
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-04-05Revert "Prevent pretyping from checking well-guardedness unnecessarily."Arnaud Spiwack
2015-09-25Prevent pretyping from checking well-guardedness unnecessarily.Arnaud Spiwack
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
2015-03-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-04Fix bug #3532, providing universe inconsistency information when aMatthieu Sozeau
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
2015-03-03Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeMatthieu Sozeau
2015-03-03Fix bug #4101, noccur_evar's expand_projection can legitimately failMatthieu Sozeau
2015-03-03Fix bug introduced by my last commit, forgetting to adjust de BruijnMatthieu Sozeau
2015-03-02Fix bug #4097.Matthieu Sozeau
2015-02-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Taking current env and not global env in b286c9f4f42f (4 commits ago,Hugo Herbelin
2015-02-27simpl: honor Global for "simpl: never" (Close: 3206)Enrico Tassi
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
2015-02-27Fixing first part of bug #3210 (inference of pattern-matching returnHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:32:07 +0000