aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-09Using self-documenting argument names in two exceptions of cases.ml.Hugo Herbelin
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ...coqbot-app[bot]
2020-11-05Fixes #13216 (use of type classes in the return clause of a match).Hugo Herbelin
2020-10-31Closes #13278: take into account elimination constraints in small inversion.Hugo Herbelin
2020-10-31Fine-tuning the sort of the predicate obtained by small inversion.Hugo Herbelin
2020-10-31Useless evar type for typing impossible case.Hugo Herbelin
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-05Wish #12762: warning on duplicated catch-all pattern with unused named variable.Hugo Herbelin
2020-07-01UIP in SPropGaëtan Gilbert
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-20Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in casesGaëtan Gilbert
2020-02-04Remove `unsafe_type_of` from `Coercion`Maxime Dénès
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-02-28Print location for type error in pattern variableGaëtan Gilbert
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08Flags of evar_conv_x/unifiers: rationalizeMatthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2019-02-05Make Program a regular attributeMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-27Merge PR #7696: Remove some univ_flexible_alg from casesPierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-16Remove some univ_flexible_alg from casesGaëtan Gilbert
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-10-14Parameterizing default inhabitant for impossible cases with an environment.Hugo Herbelin
2018-10-07[api] Deprecate `evar_map` ref combinators.Emilio Jesus Gallego Arias
2018-10-03[pretyper] Remove imperative passing of evar_map.Emilio Jesus Gallego Arias
2018-09-27Possible abstractions over goal variables when inferring match return clause.Hugo Herbelin
2018-09-27Trying an abstracting dependencies heuristic for the match return clause even...Hugo Herbelin
2018-09-27Trying a no-inversion no-dependency heuristic for match return clause.Hugo Herbelin
2018-09-27Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
2018-09-26Making cases.ml use state-passing instead of the evdref idiom.Pierre-Marie Pédrot
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
2018-09-10Relying on the precomputation of the renaming also for new_evar_type.Hugo Herbelin
2018-09-10Fixing ltac names interpretation in internals of pattern-matching compilation.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:38:21 +0000