aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Expand)AuthorAge
* Fixing incorrect change to pattern-unification over Meta's introducedGravatar herbelin2011-11-06
* Deactivating second-order pattern-matching in evarconv for 8.4.Gravatar herbelin2011-10-26
* Fixing instance/filter mismatch in materialize_evar + documentation.Gravatar herbelin2011-10-24
* Fail if some conv pbs remain after consider_remaining_unif_problems.Gravatar herbelin2011-10-22
* Use also second-order unification if first-order fails at the time of conside...Gravatar herbelin2011-10-22
* Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedGravatar herbelin2011-10-11
* More robust and uniform treatment of aliases in evarutil.mlGravatar herbelin2011-10-10
* Applied the trick of Chung-Kil Hur to solve second-order matchingGravatar herbelin2011-10-10
* Evarconv: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Ensured that the transparency state is used when flag betaiota is on for apply.Gravatar herbelin2011-06-19
* Applying Enrico Tassi's patch for giving priority to delta over eta inGravatar herbelin2011-05-24
* As remarked by Enrico, we'd better use eq_constr than structural equalityGravatar herbelin2011-03-31
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Revert commit r13883: instantiating ?n by a lambda when "?n a" has toGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Added support for instantiation of ?n by a lambda when "?n a" has toGravatar herbelin2011-03-05
* Reorganized a bit evarconv.ml:Gravatar herbelin2011-03-05
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Fix bug 2307Gravatar pboutill2010-05-20
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* change in the order of unification constraints solving (for canonical structu...Gravatar amahboub2009-07-06
* Backtrack on experimental unification with sort variables: it requires Gravatar msozeau2009-06-02
* Properly catch sort constraint inconsistency exception inGravatar msozeau2009-05-28
* Populate the sort constraints set correctly during unification. Add aGravatar msozeau2009-05-27
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* fix a bug in canonical structures (bug found and fixed by Cyril)Gravatar barras2009-05-09
* Fixes to make Ynot compile with the trunk:Gravatar msozeau2009-03-20
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* memoized is_ground_envGravatar barras2009-02-09
* pushed evar reduction in kernelGravatar barras2009-02-06
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* fixed problem with r11612Gravatar barras2008-11-21
* fixed exponential behavior of evar unif (ground case)Gravatar barras2008-11-21
* Fix universe problem appearing ConCaT using the existing infrastructure forGravatar msozeau2008-11-07
* Correction de bugs:Gravatar herbelin2008-08-05
* Suite 11187 et 11298 : ne retarder le dépliage d'une projectionGravatar herbelin2008-08-05
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Correction d'un bug dans l'analyse des contraintes non résoluesGravatar herbelin2008-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 20:30:26 +0000