aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
2007-07-12port de r9968: bug avec les ring calculatoiresbarras
2007-07-09More natural notation for intro pattern: @a -> ?aglondu
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
2007-07-06Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))letouzey
2007-07-05documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/...letouzey
2007-06-19typo faqherbelin
2007-06-08Removed an extra \tacindex occurrence for the tactic discriminate.emakarov
2007-06-07Ajout doc clear sans argumentherbelin
2007-05-17Fixed bug #1540 (typo on name .coqide-gtk2rc)herbelin
2007-05-16- MAJ entêtes des fichiers produits par coq_makefileherbelin
2007-05-11Made some places in the reference manual clearer. Correctedemakarov
2007-04-29Ajout possibilité d'options à trois mots.herbelin
2007-04-26Documentation de Existential et de Show Existential (fixes bug #1294)notin
2007-04-18Fixed some typos.glondu
2007-04-17Corrected a LaTeX typo.emakarov
2007-04-17Changed many refman/*.tex files. Put \label and \index commands that immediat...emakarov
2007-04-16Removed from headers.hva the code to make index point to the sectionemakarov
2007-04-12Cleaned doc/common/title.tex file. Increased the space under headersemakarov
2007-04-12Standardisation format biblioherbelin
2007-04-10Some changes to eliminate Hevea warnings.emakarov
2007-04-10Split refman/headers.tex into headers.sty and headers.hva.emakarov
2007-04-10Eliminated warning messages from Hevea. Most warning messages wereemakarov
2007-04-05Mise en place d'un rafinement de compute. jforest
2007-04-04Corrected a typo in doc/refman/Setoid.tex.emakarov
2007-03-16Correction du bug #1441notin
2007-03-13Correction bug #1439 (comportement de replace by)notin
2007-03-07Application suggestion #1430 de Yevgeniy pour TEXINPUTSherbelin
2007-02-22doc: typo/english: "is left associating" -> "is left-associative".lmamane
2007-02-22Documentation of tactical "t1 || t2": t2 is executed if t1 fails tolmamane
2007-02-18Compilation de la FAQnotin
2007-02-15Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lorsherbelin
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
2007-02-07Meilleur anglais (cf 9619)herbelin
2007-02-07Relecture/nettoyage chapitre Gallina; déplacement section Functionherbelin
2007-02-07Suppression RefMan-cas.tex inutiliséherbelin
2007-02-07Field rewrites only with polynomialthery
2007-02-07doc de ring/field + option infinite -> completenessbarras
2007-02-06doc for fieldthery
2007-02-05complement du commit 9591bgregoir
2007-02-01Report 9545 de 8.1 vers trunkherbelin
2007-02-01Petite relecture partie ringherbelin
2007-01-31report de r9574: doc de fieldbarras
2007-01-31Fix typo.msozeau
2007-01-31Fix order of wf and measure arguments, patch Program doc.msozeau
2007-01-26Explication du intros until nnotin
2007-01-24doc de ringbgregoir
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 19:04:10 +0000