aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Correction du bug #1785Gravatar notin2008-01-29
* Nicer proofs.Gravatar roconnor2008-01-24
* remove Fourier Failure warnings.Gravatar roconnor2008-01-24
* Prove the decidability of arithmetical statements using the real numbers.Gravatar roconnor2008-01-24
* Fermeture du bug #1754Gravatar notin2008-01-24
* Keep the Z_scope local to this file.Gravatar roconnor2008-01-24
* Changing R to a local definition so that it isn't exported.Gravatar roconnor2008-01-23
* Ajout d'un test pour le bug #1779Gravatar notin2008-01-23
* Ajout d'un test pour le mode déclaratif + test pour le bug #1776Gravatar notin2008-01-23
* TypoGravatar notin2008-01-23
* Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)Gravatar notin2008-01-22
* Adding Zdiv_le_compat_lGravatar thery2008-01-22
* Récupération d'une exception Not_foundGravatar notin2008-01-22
* Correction du bug #1754Gravatar notin2008-01-21
* cosmetics: after an extract inductive to bool, let's use if then elseGravatar letouzey2008-01-20
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...Gravatar msozeau2008-01-18
* bug in accessing n-th abstractionGravatar barras2008-01-18
* Change notation for setoid inequality, coerce objects before comparing them. ...Gravatar msozeau2008-01-18
* Fix Makefile bug, using .v instead of .vo and document SetoidDec.vGravatar msozeau2008-01-17
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* fixed script printingGravatar corbinea2008-01-17
* Bug in sqrt321Gravatar thery2008-01-17
* Fix backtracking bugs:Gravatar lmamane2008-01-15
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Amélioration de la génération des graphes de dépendancesGravatar notin2008-01-11
* implements a better way to respect the Unix convention that processes receive...Gravatar bertot2008-01-11
* Amélioration de la génération des graphes de dépendances (utilisation de ...Gravatar notin2008-01-11
* Correction du bug #1770: il semble que la recherche insensible à la casse ne...Gravatar notin2008-01-10
* Correction of bug #1769Gravatar jforest2008-01-09
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous CoqideGravatar notin2008-01-07
* Remove spurious .d, better tactics.Gravatar msozeau2008-01-07
* Completion of 10427...Gravatar herbelin2008-01-07
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* Correction bug #1749 (datant de l'implantation des or-patterns) +Gravatar herbelin2008-01-05
* Fixed bug 1761 (unexpected anomaly when constructor type has invalidGravatar herbelin2008-01-05
* Added a note about the ambiguity of the syntax "qualid" in "tacarg"Gravatar herbelin2008-01-05
* Standardisation du format des références croisées vers Figure, Section, Ch...Gravatar herbelin2008-01-05
* more user-friendly versions of some properties lemmas in FSets/FMapGravatar letouzey2008-01-04
* Add partial setoids in theories/Classes, add SetoidDec class for setoids with...Gravatar msozeau2008-01-04
* Prise en compte de CAMLP4LIB via fichier configure plutôt que dynamiquementGravatar herbelin2008-01-04
* Implicit arguments in class field declarationsGravatar msozeau2008-01-02
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Fix name capture bug and call the right pretyper in subtac.Gravatar msozeau2007-12-31
* Removed merge tracking for "svnmerge" for Gravatar msozeau2007-12-31
* Move Classes.Setoid to Classes.SetoidClass to avoid name clash.Gravatar msozeau2007-12-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Initialized merge tracking via "svnmerge" with revisions "1-10357" from Gravatar msozeau2007-12-31
* Pour éviter des erreus lors de make doc dues à du code source non taggé en...Gravatar notin2007-12-21
* Deux petits théorèmes utiles dans Minus.vGravatar notin2007-12-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 06:08:41 +0000