aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* typo faqGravatar herbelin2007-06-19
* Removed an extra \tacindex occurrence for the tactic discriminate.Gravatar emakarov2007-06-08
* Ajout doc clear sans argumentGravatar herbelin2007-06-07
* Fixed bug #1540 (typo on name .coqide-gtk2rc)Gravatar herbelin2007-05-17
* - MAJ entêtes des fichiers produits par coq_makefileGravatar herbelin2007-05-16
* Made some places in the reference manual clearer. CorrectedGravatar emakarov2007-05-11
* Ajout possibilité d'options à trois mots.Gravatar herbelin2007-04-29
* Documentation de Existential et de Show Existential (fixes bug #1294)Gravatar notin2007-04-26
* Fixed some typos.Gravatar glondu2007-04-18
* Corrected a LaTeX typo.Gravatar emakarov2007-04-17
* Changed many refman/*.tex files. Put \label and \index commands that immediat...Gravatar emakarov2007-04-17
* Removed from headers.hva the code to make index point to the sectionGravatar emakarov2007-04-16
* Cleaned doc/common/title.tex file. Increased the space under headersGravatar emakarov2007-04-12
* Standardisation format biblioGravatar herbelin2007-04-12
* Some changes to eliminate Hevea warnings.Gravatar emakarov2007-04-10
* Split refman/headers.tex into headers.sty and headers.hva.Gravatar emakarov2007-04-10
* Eliminated warning messages from Hevea. Most warning messages wereGravatar emakarov2007-04-10
* Mise en place d'un rafinement de compute. Gravatar jforest2007-04-05
* Corrected a typo in doc/refman/Setoid.tex.Gravatar emakarov2007-04-04
* Correction du bug #1441Gravatar notin2007-03-16
* Correction bug #1439 (comportement de replace by)Gravatar notin2007-03-13
* Application suggestion #1430 de Yevgeniy pour TEXINPUTSGravatar herbelin2007-03-07
* doc: typo/english: "is left associating" -> "is left-associative".Gravatar lmamane2007-02-22
* Documentation of tactical "t1 || t2": t2 is executed if t1 fails toGravatar lmamane2007-02-22
* Compilation de la FAQGravatar notin2007-02-18
* Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lorsGravatar herbelin2007-02-15
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* Meilleur anglais (cf 9619)Gravatar herbelin2007-02-07
* Relecture/nettoyage chapitre Gallina; déplacement section FunctionGravatar herbelin2007-02-07
* Suppression RefMan-cas.tex inutiliséGravatar herbelin2007-02-07
* Field rewrites only with polynomialGravatar thery2007-02-07
* doc de ring/field + option infinite -> completenessGravatar barras2007-02-07
* doc for fieldGravatar thery2007-02-06
* complement du commit 9591Gravatar bgregoir2007-02-05
* Report 9545 de 8.1 vers trunkGravatar herbelin2007-02-01
* Petite relecture partie ringGravatar herbelin2007-02-01
* report de r9574: doc de fieldGravatar barras2007-01-31
* Fix typo.Gravatar msozeau2007-01-31
* Fix order of wf and measure arguments, patch Program doc.Gravatar msozeau2007-01-31
* Explication du intros until nGravatar notin2007-01-26
* doc de ringGravatar bgregoir2007-01-24
* Correction adresse CoRN dans FAQ (suite)Gravatar herbelin2007-01-17
* Correction adresse CoRN dans FAQ (cf #1317)Gravatar herbelin2007-01-17
* Doc for Combined Scheme.Gravatar msozeau2006-12-23
* Correction typo règle réduction du fix chapitre CCIGravatar herbelin2006-12-08
* add a comment about Show Existentials and a question about case_eq Gravatar jnarboux2006-12-01
* Typo + ajout Qcanon.vGravatar herbelin2006-11-11
* Add doc on obligation solving commands.Gravatar msozeau2006-11-02
* MAJ nouvelles théoriesGravatar herbelin2006-10-28
* Documentation de "Set Printing Universes", "Print Universes" (anciennementGravatar herbelin2006-10-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 17:43:44 +0000