aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
2017-02-01Merge branch 'v8.6'Pierre-Marie Pédrot
2017-01-22Adding a new evar source to remember the name of evars which wereHugo Herbelin
2017-01-22Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).Hugo Herbelin
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-02Document changesMatthieu Sozeau
2016-11-30Fix UGraph.check_eq!Matthieu Sozeau
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-29Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).Hugo Herbelin
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-19Attempt to improve error rendering in pattern-matching compilation (#5142).Hugo Herbelin
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-13Completing reverting generalization and cleaning of the return clause inference.Hugo Herbelin
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-11Reverting generalization and cleaning of the return clause inference in v8.6.Hugo Herbelin
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-04Quick fix to #4595 (making notations containing "ltac:" unused for printing).Hugo Herbelin
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-26Posssible abstractions over goal variables when inferring match return clause.Hugo Herbelin
2016-09-26Trying an abstracting dependencies heuristic for the match return clause even...Hugo Herbelin
2016-09-26Trying a no-inversion no-dependency heuristic for match return clause.Hugo Herbelin
2016-09-26Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
2016-09-09Propagate location info on pattern match compilation.Emilio Jesus Gallego Arias
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-20Fixing a bug in the presence of let-in while inferring the return clause.Hugo Herbelin
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-06Disallow dependent case on prim records w/o etaMatthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29Program: cleanup in cases, add optionsMatthieu Sozeau
2016-06-27Rework treatment of default transparency of obligationsMatthieu Sozeau
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-27Revert "Add support for generalization also on named variables in pattern-mat...Hugo Herbelin
2016-04-27Revert "Add support for deep dependencies in variables within the recursive s...Hugo Herbelin
2016-04-27Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Hugo Herbelin
2016-04-27Revert "Using existing names as a basis for the inner names of the pattern-ma...Hugo Herbelin
2016-04-27Revert "Vers un filtrage profond ..."Hugo Herbelin
2016-04-27Vers un filtrage profond ...Hugo Herbelin
2016-04-27Using existing names as a basis for the inner names of the pattern-matching p...Hugo Herbelin
2016-04-27Fixing a De Bruijn bug in computing return predicate by inversion.Hugo Herbelin
2016-04-27Add support for deep dependencies in variables within the recursive structure.Hugo Herbelin
2016-04-27Add support for generalization also on named variables in pattern-matchingHugo Herbelin
2016-04-27Optimization in building a return clause by pattern-matching: do notHugo Herbelin
2016-03-20Splitting Evarutil in two distinct files.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 12:16:54 +0000