| Commit message (Expand) | Author | Age |
* | refined the conversion oracle | barras | 2008-05-21 |
* | Léger backtrack sur commit coqide précédent (si la commande à annuler | herbelin | 2008-05-20 |
* | - Fix bug related to indices of fixpoints. | msozeau | 2008-05-13 |
* | MAJ et bricoles diverses | herbelin | 2008-05-12 |
* | - Cleanup parsing of binders, reducing to a single production for all | msozeau | 2008-05-11 |
* | Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ] | herbelin | 2008-05-09 |
* | Mise en place d'un algorithme d'inversion des contraintes de type lors | herbelin | 2008-05-05 |
* | Réutilisation de l'infrastructure pour le polymorphisme d'univers des | herbelin | 2008-04-30 |
* | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin | 2008-04-29 |
* | - Backtrack sur option with_types suite à confusion sur l'utilisation | herbelin | 2008-04-27 |
* | - 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-26 |
* | Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve | herbelin | 2008-04-25 |
* | Change default eauto depth to 100 in setoid_rewrite, bump necessary | msozeau | 2008-04-23 |
* | Bug squashing day ! | msozeau | 2008-04-17 |
* | 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-15 |
* | Bugs, nettoyage, et améliorations diverses | herbelin | 2008-04-13 |
* | Suite 10760 | herbelin | 2008-04-05 |
* | 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-04 |
* | Ajout "simple apply" et "simple eapply" pour apply sans unfold | herbelin | 2008-04-01 |
* | Ajout d'abbréviations/notations paramétriques | herbelin | 2008-03-30 |
* | Interpret patterns for hypotheses types in match goal in type_scope (if not a | msozeau | 2008-03-25 |
* | Une passe sur les réels: | herbelin | 2008-03-23 |
* | migration of the old IntMap library from StdLib to a user contrib (Cachan/Int... | letouzey | 2008-03-19 |
* | Forget to update the CHANGES file after the commit r10180 | vsiles | 2008-03-11 |
* | Fix bugs that were reopened due to the change of setoid | msozeau | 2008-03-08 |
* | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau | 2008-03-07 |
* | Application patch #1807 sur hypothèse inutile de Rpower_O | herbelin | 2008-02-27 |
* | Essai de prise en compte de delta dans unify_0 (même sur termes non clos). | herbelin | 2008-02-13 |
* | Documentation of CHANGES and refman doc for the implicit argument binder | msozeau | 2008-02-08 |
* | Suite révision 10495 | herbelin | 2008-02-01 |
* | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau | 2008-01-17 |
* | Suite ajout raccourcis à compute et lazy pour réduire tout sauf | herbelin | 2007-11-09 |
* | Cleanup attempt of Hints in *Interface.v files. | letouzey | 2007-10-21 |
* | 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-10-03 |
* | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin | 2007-09-30 |
* | Forget to update the CHANGES file | vsiles | 2007-09-28 |
* | Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0 | herbelin | 2007-09-27 |
* | Petit complément au commit 10131. | herbelin | 2007-09-21 |
* | Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les | herbelin | 2007-09-04 |
* | New bootstrapping, improved, Makefile system | corbinea | 2007-07-13 |
* | More natural notation for intro pattern: @a -> ?a | glondu | 2007-07-09 |
* | If a fixpoint is not written with an explicit { struct ... }, then | letouzey | 2007-07-07 |
* | 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-07-06 |