aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* still one more substituion s/Set/Type/Gravatar letouzey2008-03-04
* one more substitution s/Set/Type/Gravatar letouzey2008-03-04
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* use loc instead of dummy_loc in the ugly intro-pattern rewrite hackGravatar letouzey2008-03-04
* A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)Gravatar letouzey2008-03-02
* Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_OGravatar herbelin2008-03-01
* Rework on rich forms of rewriteGravatar letouzey2008-03-01
* Petite modif pour pouvoir faire "intros until 0" qui introduit autant Gravatar aspiwack2008-02-29
* Argumentation plus poussée de pourquoi on retire la condition x>0 dansGravatar herbelin2008-02-29
* Some suggestions about FMap by P. Casteran: Gravatar letouzey2008-02-28
* Coq_makefile: correction de l'appel aux exécutables OcamlGravatar notin2008-02-28
* cardinal is promoted to the rank of primitive member of the FMap interfaceGravatar letouzey2008-02-28
* Coq_makefile: Correction d'un bug sur les options passées à CoqdocGravatar notin2008-02-28
* Do not open type_scope in SetoidClass.Gravatar msozeau2008-02-28
* Fix compilation problem (hopefully).Gravatar msozeau2008-02-28
* Nicer third spec of choose. Gravatar letouzey2008-02-28
* For more uniformity, use implicits in FSetAVLGravatar letouzey2008-02-27
* Application patch #1807 sur hypothèse inutile de Rpower_OGravatar herbelin2008-02-27
* Génération d'une toc en html et avec l'option -psGravatar notin2008-02-27
* dead codeGravatar letouzey2008-02-27
* Bug dans la génération de la stdlibGravatar notin2008-02-27
* Amélioration de la gestion des chemins physiques (corrige au passage le bug ...Gravatar notin2008-02-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 21:44:39 +0000