aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-02-27typoletouzey
2008-02-26New instance returns the (future) identifier of the instance.msozeau
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
2008-02-25coq_makefile: variablesnotin
2008-02-25coq_makefile: dépendances + génération des fichiers htmlnotin
2008-02-25Bug de coqdoc : les commentaires simples généraient des lignes videsnotin
2008-02-25Correction d'un bug de Coqdoc (indentation des lignes)notin
2008-02-25Forgotten file in previous commitlmamane
2008-02-22Merge with lmamane's private branch:lmamane
2008-02-21congruence now knows about _ -> _corbinea
2008-02-20Petits oublis dans Makefile.docnotin
2008-02-19added products and sorts as possible heads for canonical structurescorbinea
2008-02-19fixed pp for declarative modecorbinea
2008-02-18Petite correction suite à la révision 10571notin
2008-02-18Ajout de caractères unicode reconnus apr le lexernotin
2008-02-15Patch bug #1799soubiran
2008-02-15Suppression d'un include et de 2 variables inutilesnotin
2008-02-14Suspension de l'introduction de delta dans apply : certaines contribsherbelin
2008-02-14Plongement de doc/Makefile dans la nouvelle architecutre des Makefilenotin
2008-02-14Bug de Coqdoc avec l'option -Rnotin
2008-02-14Some bad emacs messup that was commited...msozeau
2008-02-14Reconnaissance des tokens dans les notations (suite à la revision r10562)notin
2008-02-14Added default canonical structures (see example in test-suite)corbinea
2008-02-14Backtrack changes on eauto, move specialized version of eauto inmsozeau
2008-02-13Move class_setoid to class_tactics.msozeau
2008-02-13Debugging of the class_setoid tactic and eauto. Prepare for move frommsozeau
2008-02-13Correction du bug #1512notin
2008-02-13Implement KEEP_ML4_PREPROCESSED option in build systemlmamane
2008-02-13Implement NO_RECALC_DEPS option in build systemlmamane
2008-02-13Suppression de l'option -glob-from de Coqdoc: les globalisations sontnotin
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
2008-02-13Correction de ce qui semble être un petit bug dans la gestion de laherbelin
2008-02-11Correction d'un bug de clearnotin
2008-02-10Fixing bug 1795 (occur check was not correctly done)herbelin
2008-02-10suppression code mort oublié lors du commit 10495herbelin
2008-02-10Granting wish 1794 (the name provided in the "using" clause of theherbelin
2008-02-10Backport Program Instance into Instance. Proper early error message ifmsozeau
2008-02-10Proposal of a nice notation for constructors xI and xO of type positiveletouzey
2008-02-10Major revision: use of Function, including some non-structural onesletouzey
2008-02-09Major revision of FSetAVL: more Function, including some non-structural onesletouzey
2008-02-09Solde de code mort et petites optimisations sur lesquels je suisherbelin
2008-02-09Fix the clrewrite tactic, change Relations.v to work on relations in Propmsozeau
2008-02-08misc improvementsletouzey
2008-02-08Documentation of CHANGES and refman doc for the implicit argument bindermsozeau
2008-02-08better comments in FMapInterfaceletouzey
2008-02-08better comments in FSetInterfaceletouzey
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
2008-02-08Add more information to IllFormedRecBody exceptions, to show the exactmsozeau
2008-02-08Move generally useful definition of nf_evar on contexts to evarutil.msozeau
2008-02-08Add printer for Pp.std_ppcmds...msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:06:03 +0000