aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
* Extraction Blacklist : a new command for avoiding conflicts with existing filesGravatar letouzey2008-12-16
* Fixes in the type classes documentation:Gravatar msozeau2008-12-14
* About "apply in":Gravatar herbelin2008-12-09
* Inductive parameters: nicer doc examples and error messageGravatar letouzey2008-11-28
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
* Fix typo in omega docGravatar glondu2008-11-19
* Document native "Declare ML Module"Gravatar glondu2008-10-29
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
* Fix doc of apply in (see coq-club message 26 September 2008)Gravatar herbelin2008-10-24
* Various coqdoc improvements:Gravatar msozeau2008-10-22
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* report de la révision r11451 (nouveau style html pour le manuel de référence)Gravatar notin2008-10-14
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Update stdlib html templateGravatar glondu2008-09-15
* A pass on documentation: Gravatar msozeau2008-09-14
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppressi...Gravatar notin2008-08-06
* correction : coqart is already publishedGravatar jnarboux2008-08-06
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Typo in docGravatar glondu2008-07-29
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
* - Rebranchement backtrack du langage déclaratif dans CoqideGravatar herbelin2008-07-18
* - Suppression de Rstar/Newman peu utilisables comme biblio (encodageGravatar herbelin2008-07-17
* update doc MicromegaGravatar fbesson2008-07-13
* Documentation fixes. Gravatar msozeau2008-07-09
* Micromega: doc + test-suite updateGravatar fbesson2008-07-07
* Improved robustness of micromega parser. Proof search of Micromega test-suite...Gravatar fbesson2008-07-02
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
* correction sur la doc des modulesGravatar soubiran2008-07-01
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* Micromega : bugs fixes - renaming of tactics - documentationGravatar fbesson2008-06-25
* Typo in documentation (isn't it?)Gravatar glondu2008-06-25
* Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...Gravatar soubiran2008-06-25
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Numéros de version dans la docGravatar notin2008-06-13
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* 2-3 petites modifs sur la docGravatar notin2008-06-10
* Fix a typoGravatar glondu2008-06-09
* Documentation de "instantiate".Gravatar glondu2008-06-09
* - Documentation de admit et Print Assumptions.Gravatar herbelin2008-06-09
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Second pass on typeclasses documentation, fix html rendering.Gravatar msozeau2008-06-08
* Fix library index template and associated script.Gravatar msozeau2008-06-07
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
* remove additional occurrences of +/- forgotten in commit 11030Gravatar letouzey2008-06-01