aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
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
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-07-25Optimized dependencies for pattern-matching on only trivial patterns.Hugo Herbelin
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2018-06-15Better elaboration of pattern-matchings on primitive projectionsMatthieu Sozeau
2018-06-14Fix deprecation warning introduced by PR 664 mergeMatthieu Sozeau
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...Matthieu Sozeau
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-04Merge PR #7189: Fix #5539: algebraic universe produced by cases.Matthieu Sozeau
2018-06-04Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Matthieu Sozeau
2018-05-14Use evd_combX in Cases.Gaëtan Gilbert
2018-05-11Deprecate Evarconv.e_conv,e_cumulGaëtan Gilbert
2018-05-11Deprecate most evarutil evdref functionsGaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-10Replace uses of Termops.dependent by more specific functions.Pierre-Marie Pédrot
2018-04-06Fix #5539: algebraic universe produced by cases.Gaëtan Gilbert
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-27Fixing #5547 (typability of return predicate in nested pattern-matching).Hugo Herbelin
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:13:44 +0000