aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* patch for C code of addmuldiv31Gravatar thery2008-02-27
* typoGravatar letouzey2008-02-27
* New instance returns the (future) identifier of the instance.Gravatar msozeau2008-02-26
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* coq_makefile: variablesGravatar notin2008-02-25
* coq_makefile: dépendances + génération des fichiers htmlGravatar notin2008-02-25
* Bug de coqdoc : les commentaires simples généraient des lignes videsGravatar notin2008-02-25
* Correction d'un bug de Coqdoc (indentation des lignes)Gravatar notin2008-02-25
* Forgotten file in previous commitGravatar lmamane2008-02-25
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* 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