aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Expand)AuthorAge
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* Reenable FO unification of primitive projections and their eta-expandedGravatar Matthieu Sozeau2014-10-15
* Modify the heuristic for unfolding lhs or rhs in evarconv, consideringGravatar Matthieu Sozeau2014-10-15
* English typo in a function name of evarconv.Gravatar Hugo Herbelin2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Do not expand primitive projections eagerly in evarconv, but onlyGravatar Matthieu Sozeau2014-10-10
* Fixing the anomaly in bug #3045 (a filter was not type-safe inGravatar Hugo Herbelin2014-10-08
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Gravatar Matthieu Sozeau2014-10-02
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix canonical structure resolution which was launched on the results ofGravatar Matthieu Sozeau2014-09-26
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* 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
* Fix bug #3594: eta for constructors and functions at the same time whichGravatar Matthieu Sozeau2014-09-11
* Fix bug #3589, unification looping due to incorrect use of stack with primiti...Gravatar Matthieu Sozeau2014-09-08
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* In evarconv, do first-order unification of LetIn's properly, ensuring we comp...Gravatar Matthieu Sozeau2014-09-01
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* There are some occurs-check cases that can be handled by imitation (using pru...Gravatar Matthieu Sozeau2014-08-28
* Make evarconv and unification able to handle eta for records in presenceGravatar Matthieu Sozeau2014-08-26
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Restrict eta-conversion to inductive records, fixing bug #3310.Gravatar Matthieu Sozeau2014-08-14
* Fix bug introduced by earlier commit on first-order unification of primitiveGravatar Matthieu Sozeau2014-08-10
* Fix unification which was failing when unifying a primitive projection againstGravatar Matthieu Sozeau2014-08-09
* Fix evarconv not applying eta when it used to. Fixes bug#3319.Gravatar Matthieu Sozeau2014-08-08
* Revert patch making the oracle be used for the transparent state in evarconv,Gravatar Matthieu Sozeau2014-07-09
* In flex-flex cases, the undefinedness of an evar can not be preseved after co...Gravatar Matthieu Sozeau2014-07-07
* Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Gravatar Matthieu Sozeau2014-07-03
* Use full transparent state when checking well-typedness of a second order mat...Gravatar Matthieu Sozeau2014-06-25
* Reinstate eta for records in evarconv, fixing two HoTT coq bugs.Gravatar Matthieu Sozeau2014-06-17
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Adapt simpl/cbn unfolding and refolding machinery to projections, so thatGravatar Matthieu Sozeau2014-06-13
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Fix canonical structure resolution in unification (bug found in Ssreflect).Gravatar Matthieu Sozeau2014-06-08
* Fix canonical structure resolution (makes test-suite files go through again).Gravatar Matthieu Sozeau2014-06-04
* More fixes of unification with primitive projections (missed cases during the...Gravatar Matthieu Sozeau2014-05-16
* Fix unification of non-unfoldable primitive projections in evarconv.Gravatar Matthieu Sozeau2014-05-16
* Fix second-order matching to properly check that the predicate found byGravatar Matthieu Sozeau2014-05-09
* - Add back some compatibility functions to avoid rewriting plugins.Gravatar Matthieu Sozeau2014-05-06
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* In case two constants/vars/rels are _not_ defined, force unification of unive...Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 16:33:26 +0000