aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2009-01-21Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824herbelin
2009-01-20Added some missing statements for proof folding and correctedvgross
2009-01-20Added proof folding into CoqIde. See RefMan for using it.vgross
2009-01-19Propriétés svn pour les filtres latexnotin
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-18Last changes in type class syntax: msozeau
2009-01-13Updated datesherbelin
2009-01-13- Standardized prefix use of "Local"/"Global" modifiers as decided inherbelin
2009-01-08Minor doc fixes:msozeau
2009-01-03Fixed two problems:herbelin
2009-01-01- Fixed bug #2021 (uncaught exception with injection/discriminate whenherbelin
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-12-29Produce better html code with coqdoc and improve doc:msozeau
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
2008-12-16Extraction Blacklist : a new command for avoiding conflicts with existing filesletouzey
2008-12-14Fixes in the type classes documentation:msozeau
2008-12-09About "apply in":herbelin
2008-11-28Inductive parameters: nicer doc examples and error messageletouzey
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
2008-11-19Fix typo in omega docglondu
2008-10-29Document native "Declare ML Module"glondu
2008-10-27- Fixed many "Theorem with" bugs.herbelin
2008-10-24Fix doc of apply in (see coq-club message 26 September 2008)herbelin
2008-10-22Various coqdoc improvements:msozeau
2008-10-20Renommage "Global Instance" en "Instance Global" pour uniformisationherbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-10-14report de la révision r11451 (nouveau style html pour le manuel de référence)notin
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-09-15Update stdlib html templateglondu
2008-09-14A pass on documentation: msozeau
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
2008-08-06Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppressi...notin
2008-08-06correction : coqart is already publishedjnarboux
2008-08-04Évolutions diverses et variées.herbelin
2008-07-29Typo in docglondu
2008-07-23Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theherbelin
2008-07-18- Rebranchement backtrack du langage déclaratif dans Coqideherbelin
2008-07-17- Suppression de Rstar/Newman peu utilisables comme biblio (encodageherbelin
2008-07-13update doc Micromegafbesson
2008-07-09Documentation fixes. msozeau
2008-07-07Micromega: doc + test-suite updatefbesson
2008-07-02Improved robustness of micromega parser. Proof search of Micromega test-suite...fbesson
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
2008-07-01correction sur la doc des modulessoubiran
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2008-06-25Micromega : bugs fixes - renaming of tactics - documentationfbesson
2008-06-25Typo in documentation (isn't it?)glondu
2008-06-25Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...soubiran
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:44:57 +0000