aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
AgeCommit message (Expand)Author
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-22Renamings to avoid confusion deprecating old namesMatthieu Sozeau
2016-10-22Unification constraint handling (#4763, #5149)Matthieu Sozeau
2016-10-22Port fix for bugs 4763, 5149, previously 0b417c12eMatthieu Sozeau
2016-10-21Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-10-21Revert "unification.ml: fix for bug #4763, unif regression"Maxime Dénès
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-08Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-06w_merge: Add a comment about the (List.rev evars)Matthieu Sozeau
2016-10-06unification.ml: fix for bug #4763, unif regressionMatthieu Sozeau
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-03Merge remote-tracking branch 'github/pr/263' into v8.6Maxime Dénès
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-22Fixing #5095 (non relevant too strict test in let-in abstraction).Hugo Herbelin
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-09no-refold patchPaul Steckler
2016-09-09Tracking careless uses of slow name lookup.Pierre-Marie Pédrot
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-25Merge remote-tracking branch 'v8.6' into trunkMatej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-22Pushing error backtrace in unification reraise.Pierre-Marie Pédrot
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-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
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-10A mini-optimization for free in unification.ml: test in O(1)Hugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-03-20Splitting Evarutil in two distinct files.Pierre-Marie Pédrot
2016-03-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-17Fix #4623: set tactic too weak with universes (regression)Maxime Dénès
2016-03-15Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-14Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-23Fix part of bug #4533: respect declared global transparency ofMatthieu Sozeau
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-02-03Optimizing the computation of frozen evars.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-12Extend last commit: keyed unification uses full conversions on the applied co...Matthieu Sozeau
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-11Ensure that conversion is called on terms of the same type inMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:37:30 +0000