aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* fixed bug #1780: a lift was missing (match predicate)Gravatar barras2008-05-29
* Notation concise pour la valeur par défaut des cas reconnus commeGravatar herbelin2008-05-28
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...Gravatar barras2008-05-28
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
* - Fix bug #1858, Hint Unfold calling the wrong locate function.Gravatar msozeau2008-05-23
* refined the conversion oracleGravatar barras2008-05-21
* Correction d'un bug de l'unification pattern qui oubliait d'expanserGravatar herbelin2008-05-20
* Better implementation of the set of instances of a given class as a CmapGravatar msozeau2008-05-15
* Résolution des problèmes ambigus d'inférence du type de retour desGravatar herbelin2008-05-14
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* Correction du bug des types singletons pas sous-type de SetGravatar 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
* 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