aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-02-28Coq_makefile: correction de l'appel aux exécutables Ocamlnotin
2008-02-28cardinal is promoted to the rank of primitive member of the FMap interfaceletouzey
2008-02-28Coq_makefile: Correction d'un bug sur les options passées à Coqdocnotin
2008-02-28Do not open type_scope in SetoidClass.msozeau
2008-02-28Fix compilation problem (hopefully).msozeau
2008-02-28Nicer third spec of choose. letouzey
2008-02-27For more uniformity, use implicits in FSetAVLletouzey
2008-02-27Application patch #1807 sur hypothèse inutile de Rpower_Oherbelin
2008-02-27Génération d'une toc en html et avec l'option -psnotin
2008-02-27dead codeletouzey
2008-02-27Bug dans la génération de la stdlibnotin
2008-02-27Amélioration de la gestion des chemins physiques (corrige au passage le bug ...notin
2008-02-27patch for C code of addmuldiv31thery
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 11:19:39 +0000