aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
Commit message (Expand)AuthorAge
...
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Fix bug #3505.Gravatar Matthieu Sozeau2014-09-11
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Fix bugs #3484 and #3546.Gravatar Matthieu Sozeau2014-08-28
* Fixing an unnatural selection of subterms larger than expected in theGravatar Hugo Herbelin2014-08-28
* Make evarconv and unification able to handle eta for records in presenceGravatar Matthieu Sozeau2014-08-26
* Fix compilation error due to commented code in previous commit by Hugo.Gravatar Matthieu Sozeau2014-08-26
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Fixing unification of subterms identified by patterns.Gravatar Hugo Herbelin2014-08-18
* Refine patch for behavior of unify_to_subterm to allow backtracking onGravatar Matthieu Sozeau2014-08-18
* Remove confusing behavior of unify_with_subterm that could fail withGravatar Matthieu Sozeau2014-08-14
* Do early occur-check in unification to allow eta to fire (fixes bug #3477)Gravatar Matthieu Sozeau2014-08-09
* - Fix has_undefined_evars not using its or_sorts argument anymore.Gravatar Matthieu Sozeau2014-08-03
* Revert patch making the oracle be used for the transparent state in evarconv,Gravatar Matthieu Sozeau2014-07-09
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Extra check for indirect dependency when abstracting a term which isGravatar Hugo Herbelin2014-06-28
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* Use the right transparent state when comparing _types_ of metas.Gravatar Matthieu Sozeau2014-06-25
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* - Fix bug in unification, not only named metas are turned into evars (e.g. in...Gravatar Matthieu Sozeau2014-06-19
* Improved error message when a meta posed as an evar remains unsolvedGravatar Hugo Herbelin2014-06-13
* Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Gravatar Hugo Herbelin2014-06-13
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* - Allow parsing of @const@{instance} for specifying universe instances of pol...Gravatar Matthieu Sozeau2014-06-04
* - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someGravatar Matthieu Sozeau2014-05-28
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Fix second-order matching to properly check that the predicate found byGravatar Matthieu Sozeau2014-05-09
* Fix performance problem with unification in presence of universes (bug #3302)...Gravatar Matthieu Sozeau2014-05-08
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Reductionops.Stack.strip* are ready to deal with ShiftGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Optimization in unification: when checking that the head of a term is anGravatar ppedrot2013-10-29
* Useless array-to-list casts in Unification.Gravatar ppedrot2013-10-29
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* - install evar printer for debuggingGravatar msozeau2013-10-29
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-18 04:30:40 +0000