aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
2008-03-04use loc instead of dummy_loc in the ugly intro-pattern rewrite hackletouzey
2008-03-02A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)letouzey
2008-03-01Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_Oherbelin
2008-03-01Rework on rich forms of rewriteletouzey
2008-02-29Petite modif pour pouvoir faire "intros until 0" qui introduit autant aspiwack
2008-02-29Argumentation plus poussée de pourquoi on retire la condition x>0 dansherbelin
2008-02-28Some suggestions about FMap by P. Casteran: letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 04:29:15 +0000