aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
AgeCommit message (Expand)Author
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-28Fix bugs #3484 and #3546.Matthieu Sozeau
2014-08-28Fixing an unnatural selection of subterms larger than expected in theHugo Herbelin
2014-08-26Make evarconv and unification able to handle eta for records in presenceMatthieu Sozeau
2014-08-26Fix compilation error due to commented code in previous commit by Hugo.Matthieu Sozeau
2014-08-25Fixing the essence of naming bug #3204: use same strategy for namingHugo Herbelin
2014-08-22Move UnsatisfiableConstraints to a pretype error.Matthieu Sozeau
2014-08-18Fixing unification of subterms identified by patterns.Hugo Herbelin
2014-08-18Refine patch for behavior of unify_to_subterm to allow backtracking onMatthieu Sozeau
2014-08-14Remove confusing behavior of unify_with_subterm that could fail withMatthieu Sozeau
2014-08-09Do early occur-check in unification to allow eta to fire (fixes bug #3477)Matthieu Sozeau
2014-08-03- Fix has_undefined_evars not using its or_sorts argument anymore.Matthieu Sozeau
2014-07-09Revert patch making the oracle be used for the transparent state in evarconv,Matthieu Sozeau
2014-06-28Moved code for finding subterms (pattern, induction, set, generalize, ...)Hugo Herbelin
2014-06-28Extra check for indirect dependency when abstracting a term which isHugo Herbelin
2014-06-28Made the subterm finding function make_abstraction independent of theHugo Herbelin
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
2014-06-25Use the right transparent state when comparing _types_ of metas.Matthieu Sozeau
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
2014-06-19- Fix bug in unification, not only named metas are turned into evars (e.g. in...Matthieu Sozeau
2014-06-13Improved error message when a meta posed as an evar remains unsolvedHugo Herbelin
2014-06-13Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Hugo Herbelin
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-04- Allow parsing of @const@{instance} for specifying universe instances of pol...Matthieu Sozeau
2014-05-28- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someMatthieu Sozeau
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-09Fix second-order matching to properly check that the predicate found byMatthieu Sozeau
2014-05-08Fix performance problem with unification in presence of universes (bug #3302)...Matthieu Sozeau
2014-05-06- Fixes for canonical structure resolution (check that the initial term indee...Matthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06- Fix comparison of universes.Matthieu Sozeau
2014-05-06Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-02-24Reductionops.Stack.strip* are ready to deal with ShiftPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-29Optimization in unification: when checking that the head of a term is anppedrot
2013-10-29Useless array-to-list casts in Unification.ppedrot
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
2013-10-29- install evar printer for debuggingmsozeau
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-23Small optimizations in unification.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-07-19- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...msozeau
2013-06-19- Keep the refinement of existing evars comming from unification with a rewri...msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:04:09 +0000