aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* - 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
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* 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
* Add the ability to give a transparent_state for conversion, toGravatar msozeau2008-04-20
* Correction bug 1835 + correction bug occur-check résultant en unGravatar herbelin2008-04-18
* Bug squashing day !Gravatar msozeau2008-04-17
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* Mises à jour bugs, CHANGES, code mortGravatar herbelin2008-04-15
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Diverses corrections Gravatar herbelin2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Document the new setoid rewrite tactic, and fix a few things whileGravatar msozeau2008-04-12
* Fix evar bugs in type classes:Gravatar msozeau2008-04-09
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
* - Relâchement de la contrainte de bonne longueur des intropatternsGravatar herbelin2008-04-04
* Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiGravatar herbelin2008-04-04
* Essai d'un peu plus de conversion dans apply : suppression de laGravatar herbelin2008-04-03
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* Finish enhancemenent of return clause inference from tycons, integratingGravatar msozeau2008-04-01
* Modifications diverses et variées :Gravatar herbelin2008-03-30
* Fix test-suite files, change conflicting notation "->rel" and the othersGravatar msozeau2008-03-29
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Correct bug introduced in r10589, where we lost information thatGravatar msozeau2008-03-21
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Add the possibility of specifying constants to unfold for typeclassGravatar msozeau2008-03-17
* * Factorizing code : context_chop was used in several files (even as chop_con...Gravatar vsiles2008-03-17
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
* Typo commit 10653Gravatar herbelin2008-03-11
* Pas très propre de reposer sur la capture des anomalies (et celaGravatar herbelin2008-03-10
* fold travaille maintenant sur la forme beta-iota-zeta réduite duGravatar herbelin2008-03-10
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* 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
* Petite modif pour pouvoir faire "intros until 0" qui introduit autant Gravatar aspiwack2008-02-29
* added products and sorts as possible heads for canonical structuresGravatar corbinea2008-02-19
* Suspension de l'introduction de delta dans apply : certaines contribsGravatar herbelin2008-02-14
* Added default canonical structures (see example in test-suite)Gravatar corbinea2008-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
* Correction d'un bug de clearGravatar notin2008-02-11