aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
Commit message (Expand)AuthorAge
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Fixing bug #1918 (no occur-check in Meta unification was done yet!).Gravatar herbelin2009-01-20
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Fixes for unification and substitution of metas under binders.Gravatar msozeau2008-12-04
* Miscellaneous fixes and improvements:Gravatar herbelin2008-12-02
* Restores behaviour of v8.1 for unification problems which fail (backport of 1...Gravatar letouzey2008-11-14
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* * Fixed constr_cmp again to handle universes subtyping correctlyGravatar puech2008-10-09
* (Try to) use the conversion oracle also in w_unify to choose which constant toGravatar msozeau2008-10-03
* Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anGravatar msozeau2008-09-04
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)Gravatar herbelin2008-06-21
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)Gravatar barras2008-06-05
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...Gravatar barras2008-05-28
* refined the conversion oracleGravatar barras2008-05-21
* Correction d'un bug de l'unification pattern qui oubliait d'expanserGravatar herbelin2008-05-20
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bug squashing day !Gravatar msozeau2008-04-17
* - Relâchement de la contrainte de bonne longueur des intropatternsGravatar herbelin2008-04-04
* Essai d'un peu plus de conversion dans apply : suppression de laGravatar herbelin2008-04-03
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* Modifications diverses et variées :Gravatar herbelin2008-03-30
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Toujours suite commits 10623 et 10624:Gravatar herbelin2008-03-06
* Suite commit 10623:Gravatar herbelin2008-03-06
* Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?nGravatar herbelin2008-03-06
* Correction d'une typo restant du commit 10557 et cause d'échec de contribsGravatar herbelin2008-03-05
* Suspension de l'introduction de delta dans apply : certaines contribsGravatar herbelin2008-02-14
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Correction de ce qui semble être un petit bug dans la gestion de laGravatar herbelin2008-02-13
* Mise en place d'une toute petite amélioration de l'unification deGravatar herbelin2008-02-07
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
* Unification des types + clause filtrage manquante + uniformisation localeGravatar herbelin2007-06-07
* Toujours l'unification de apply : nouveau raffinement pour ne testerGravatar herbelin2007-06-06
* Amélioration de la complexité de auto (l'utilisation des types dansGravatar herbelin2007-06-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 23:45:08 +0000