aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
AgeCommit message (Expand)Author
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
2015-11-10Revert "Fixing #1225: we now skip the canonically built binding contexts of"Hugo Herbelin
2015-11-10Fixing #1225: we now skip the canonically built binding contexts ofHugo Herbelin
2015-10-19More monotonicity in Tactics.Pierre-Marie Pédrot
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-09-27Removing subst_defined_metas_evars from Evd.Pierre-Marie Pédrot
2015-07-16Refining 71def2f8 on too strong occur-check limiting evar-evarHugo Herbelin
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-02-23Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Hugo Herbelin
2015-02-23Fixing occur-check which was too strong in unification.ml.Hugo Herbelin
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-30Simplifying second_order_matching: no need to invert the linearHugo Herbelin
2014-12-15New try on Fixing an evar_map bug revealed by commit 603b66f81 onHugo Herbelin
2014-12-15Documenting check_record + changing a possibly undefined int into int option.Hugo Herbelin
2014-12-12Two fixes in unification (bugs #3782 and #3709)Matthieu Sozeau
2014-12-11Commit not ready. Sorry.Hugo Herbelin
2014-12-11Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Hugo Herbelin
2014-12-05Fix debugger Tactic Unification.Hugo Herbelin
2014-12-05Small cleaning and uniformization in unification flags:Hugo Herbelin
2014-11-27Reverting the following block of three commits:Hugo Herbelin
2014-11-26Fixing Coq compilation.Pierre-Marie Pédrot
2014-11-26Experimenting always forcing convertibility on strict implicit argumentsHugo Herbelin
2014-11-25A bit more information in debug tactic unification.Hugo Herbelin
2014-11-25Experimenting using unification when matching evar/meta free subtermsHugo Herbelin
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-11Accepting conversion on inner closed subterms while looking forHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:25:08 +0000