aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Doc updateGravatar msozeau2007-10-24
* Added the doc for the new Scheme Equality commandGravatar vsiles2007-10-16
* documentation of commit 10188Gravatar letouzey2007-10-08
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
* Fix a problem doing 'make clean' under WinodwsGravatar notin2007-10-02
* Changes in Backtrack documentation. More accurate.Gravatar courtieu2007-09-25
* Added the documentation for Backtrack and BackTo.Gravatar courtieu2007-09-24
* Indication de quel type de constantes est dépliable dans "simpl" (cfGravatar herbelin2007-09-19
* MAJ date copyright docGravatar herbelin2007-09-18
* A word on the measure and wf modifiersGravatar msozeau2007-09-01
* Mise à jour des paramètres Whelp et ajouts d'options Set Whelp ServerGravatar herbelin2007-08-30
* Add info on measure based defs.Gravatar msozeau2007-08-26
* Save IS NOT the same Defined ....Gravatar msozeau2007-08-22
* Erreur de copier/coller dans la section GuardedGravatar notin2007-08-20
* Correction du bug #1635Gravatar notin2007-08-13
* Modification de control_only_guard, qui utilise maintenantGravatar notin2007-08-09
* A better Program documentation. Include it in the generated stdlib doc.Gravatar msozeau2007-08-08
* Move Program tactics into a proper theories/ directory as they are general pu...Gravatar msozeau2007-08-07
* Corrected the reference to glob.dump, which is used to create stdlib/index-bo...Gravatar emakarov2007-07-26
* Modifications de la construction de la documentation de la librairieGravatar notin2007-07-25
* Documentation of Program and its tactics, fix enormous interaction bug due to...Gravatar msozeau2007-07-19
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
* port de r9968: bug avec les ring calculatoiresGravatar barras2007-07-12
* More natural notation for intro pattern: @a -> ?aGravatar glondu2007-07-09
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
* Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))Gravatar letouzey2007-07-06
* documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/...Gravatar letouzey2007-07-05
* 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