aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Chgts mineurs:Gravatar herbelin2008-04-03
* Add option to set the opacity of obligations to transparent, to be ableGravatar msozeau2008-04-01
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Fix examples in Program documentation and add comindexes for the variousGravatar msozeau2008-03-23
* some references to IntMap forgotten in last commitGravatar letouzey2008-03-19
* migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...Gravatar letouzey2008-03-19
* Indexation de pose proof, et par la même occasion du nouveau specializeGravatar herbelin2008-03-10
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* repair for commit 10612 (due to grammar order, some syntaxes weren't working) Gravatar letouzey2008-03-06
* Rework on rich forms of rewriteGravatar letouzey2008-03-01
* Bug dans la génération de la stdlibGravatar notin2008-02-27
* Plongement de doc/Makefile dans la nouvelle architecutre des MakefileGravatar notin2008-02-14
* Suppression de l'option -glob-from de Coqdoc: les globalisations sontGravatar notin2008-02-13
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* Documentation of CHANGES and refman doc for the implicit argument binderGravatar msozeau2008-02-08
* New "Preterm [ of id ] " command to show the preterm before giving it toGravatar msozeau2008-02-08
* updates concerning FSetsGravatar letouzey2008-02-08
* - Documentation des nouvelles options d'implicites (Set Strongly StrictGravatar herbelin2008-02-06
* Add new files theories/Program/Basics.v and theories/Classes/Relations.vGravatar msozeau2008-02-03
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Finish let| implementation and document itGravatar msozeau2008-01-31
* Added full documentation for mathematical mode (draft version)Gravatar corbinea2008-01-29
* Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous CoqideGravatar notin2008-01-07
* Added a note about the ambiguity of the syntax "qualid" in "tacarg"Gravatar herbelin2008-01-05
* Standardisation du format des références croisées vers Figure, Section, Ch...Gravatar herbelin2008-01-05
* Maj du lien vers coq-bugs dans Coqide.Gravatar glondu2007-12-18
* Modification de la question no 172 de la FAQ (cf bug #1755)Gravatar notin2007-12-11
* Ajout de l'axiomatisation des entiers à la documentation de la librairie sta...Gravatar notin2007-11-28
* 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