| Age | Commit message (Expand) | Author |
|---|
| 2008-05-05 | Mise en place d'un algorithme d'inversion des contraintes de type lors | herbelin |
| 2008-04-30 | Réutilisation de l'infrastructure pour le polymorphisme d'univers des | herbelin |
| 2008-04-29 | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin |
| 2008-04-27 | - Backtrack sur option with_types suite à confusion sur l'utilisation | herbelin |
| 2008-04-26 | - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec | herbelin |
| 2008-04-26 | Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour | herbelin |
| 2008-04-25 | Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve | herbelin |
| 2008-04-23 | Change default eauto depth to 100 in setoid_rewrite, bump necessary | msozeau |
| 2008-04-17 | Bug squashing day ! | msozeau |
| 2008-04-15 | Mises à jour bugs, CHANGES, code mort | herbelin |
| 2008-04-15 | Document CHANGES in setoid rewrite, move DefaultRelation to | msozeau |
| 2008-04-15 | - Un peu de doc, préparation du CHANGES pour la release. | herbelin |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-04-05 | Suite 10760 | herbelin |
| 2008-04-04 | Mise en place d'une extension de apply pour que celui-ci sache | herbelin |
| 2008-04-04 | Quelques améliorations des intro patterns: | herbelin |
| 2008-04-01 | Ajout "simple apply" et "simple eapply" pour apply sans unfold | herbelin |
| 2008-03-30 | Ajout d'abbréviations/notations paramétriques | herbelin |
| 2008-03-25 | Interpret patterns for hypotheses types in match goal in type_scope (if not a | msozeau |
| 2008-03-23 | Une passe sur les réels: | herbelin |
| 2008-03-19 | migration of the old IntMap library from StdLib to a user contrib (Cachan/Int... | letouzey |
| 2008-03-11 | Forget to update the CHANGES file after the commit r10180 | vsiles |
| 2008-03-08 | Fix bugs that were reopened due to the change of setoid | msozeau |
| 2008-03-07 | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau |
| 2008-02-27 | Application patch #1807 sur hypothèse inutile de Rpower_O | herbelin |
| 2008-02-13 | Essai de prise en compte de delta dans unify_0 (même sur termes non clos). | herbelin |
| 2008-02-08 | Documentation of CHANGES and refman doc for the implicit argument binder | msozeau |
| 2008-02-01 | Suite révision 10495 | herbelin |
| 2008-01-17 | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau |
| 2007-11-09 | Suite ajout raccourcis à compute et lazy pour réduire tout sauf | herbelin |
| 2007-10-21 | Cleanup attempt of Hints in *Interface.v files. | letouzey |
| 2007-10-03 | Révision de theories/Logic concernant les axiomes de descriptions. | herbelin |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-09-30 | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin |
| 2007-09-28 | Forget to update the CHANGES file | vsiles |
| 2007-09-27 | Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0 | herbelin |
| 2007-09-21 | Petit complément au commit 10131. | herbelin |
| 2007-09-04 | Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les | herbelin |
| 2007-07-13 | New bootstrapping, improved, Makefile system | corbinea |
| 2007-07-09 | More natural notation for intro pattern: @a -> ?a | glondu |
| 2007-07-07 | If a fixpoint is not written with an explicit { struct ... }, then | letouzey |
| 2007-07-06 | a few works about my commits since February | letouzey |
| 2007-07-06 | Documentation for commit 9774. | glondu |
| 2007-07-06 | New intro pattern "@A", which generates a fresh name based on A. | glondu |
| 2007-06-30 | - Ajout de la possibilité d'utiliser la notation Record pour les | herbelin |
| 2007-05-28 | Réaffichage des Structure/Record sous la forme Record | herbelin |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-06 | Nouveaux changements autour des implicites (notamment suite à | herbelin |
| 2007-04-29 | Suite commit 9810 | herbelin |
| 2007-04-28 | Ajout de la possibilité de faire référence dans certains cas à un nom | herbelin |
