aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* congruence now knows about _ -> _Gravatar corbinea2008-02-21
* Petits oublis dans Makefile.docGravatar notin2008-02-20
* added products and sorts as possible heads for canonical structuresGravatar corbinea2008-02-19
* fixed pp for declarative modeGravatar corbinea2008-02-19
* Petite correction suite à la révision 10571Gravatar notin2008-02-18
* Ajout de caractères unicode reconnus apr le lexerGravatar notin2008-02-18
* Patch bug #1799Gravatar soubiran2008-02-15
* Suppression d'un include et de 2 variables inutilesGravatar notin2008-02-15
* Suspension de l'introduction de delta dans apply : certaines contribsGravatar herbelin2008-02-14
* Plongement de doc/Makefile dans la nouvelle architecutre des MakefileGravatar notin2008-02-14
* Bug de Coqdoc avec l'option -RGravatar notin2008-02-14
* Some bad emacs messup that was commited...Gravatar msozeau2008-02-14
* Reconnaissance des tokens dans les notations (suite à la revision r10562)Gravatar notin2008-02-14
* Added default canonical structures (see example in test-suite)Gravatar corbinea2008-02-14
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
* Move class_setoid to class_tactics.Gravatar msozeau2008-02-13
* Debugging of the class_setoid tactic and eauto. Prepare for move fromGravatar msozeau2008-02-13
* Correction du bug #1512Gravatar notin2008-02-13
* Implement KEEP_ML4_PREPROCESSED option in build systemGravatar lmamane2008-02-13
* Implement NO_RECALC_DEPS option in build systemGravatar lmamane2008-02-13
* Suppression de l'option -glob-from de Coqdoc: les globalisations sontGravatar notin2008-02-13
* 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
* Fixing bug 1795 (occur check was not correctly done)Gravatar herbelin2008-02-10
* suppression code mort oublié lors du commit 10495Gravatar herbelin2008-02-10
* Granting wish 1794 (the name provided in the "using" clause of theGravatar herbelin2008-02-10
* Backport Program Instance into Instance. Proper early error message ifGravatar msozeau2008-02-10
* Proposal of a nice notation for constructors xI and xO of type positiveGravatar letouzey2008-02-10
* Major revision: use of Function, including some non-structural onesGravatar letouzey2008-02-10
* Major revision of FSetAVL: more Function, including some non-structural onesGravatar letouzey2008-02-09
* Solde de code mort et petites optimisations sur lesquels je suisGravatar herbelin2008-02-09
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* misc improvementsGravatar letouzey2008-02-08
* Documentation of CHANGES and refman doc for the implicit argument binderGravatar msozeau2008-02-08
* better comments in FMapInterfaceGravatar letouzey2008-02-08
* better comments in FSetInterfaceGravatar letouzey2008-02-08
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
* Add more information to IllFormedRecBody exceptions, to show the exactGravatar msozeau2008-02-08
* Move generally useful definition of nf_evar on contexts to evarutil.Gravatar msozeau2008-02-08
* Add printer for Pp.std_ppcmds...Gravatar msozeau2008-02-08
* New "Preterm [ of id ] " command to show the preterm before giving it toGravatar msozeau2008-02-08
* Backport code from command.ml to subtac_command.ml for defininingGravatar msozeau2008-02-08
* more complete FSets.vGravatar letouzey2008-02-08
* updates concerning FSetsGravatar letouzey2008-02-08
* one forgotten compatibility lemmaGravatar letouzey2008-02-08
* Oubli dans r10524Gravatar notin2008-02-08
* Correction d'un bug de Coqdoc + ajout de Include dans les mots clés reconnus...Gravatar notin2008-02-08
* Mise en place d'une toute petite amélioration de l'unification deGravatar herbelin2008-02-07
* Suite 10518Gravatar herbelin2008-02-06