aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
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
2008-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-13Numéros de version dans la docnotin
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-102-3 petites modifs sur la docnotin
2008-06-09Fix a typoglondu
2008-06-09Documentation de "instantiate".glondu
2008-06-09- Documentation de admit et Print Assumptions.herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-08Second pass on typeclasses documentation, fix html rendering.msozeau
2008-06-07Fix library index template and associated script.msozeau
2008-06-03Fix setoid_rewrite documentation examples.msozeau
2008-06-01Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inletouzey
2008-06-01remove additional occurrences of +/- forgotten in commit 11030letouzey
2008-06-01Bactrack sur +, - dans rewrite qui, redondants avec ->, <-, n'en sont qu'àherbelin
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
2008-05-26Fix bashism in doc generation.glondu
2008-05-23doc of coqchk + improved module cache and computation of module setsbarras
2008-05-23Nouvelle doc pour les modules.soubiran
2008-05-22Strategy commands are now exportedbarras
2008-05-21refined the conversion oraclebarras
2008-05-19MAJ créditsherbelin
2008-05-13- Fix bug related to indices of fixpoints.msozeau
2008-05-12MAJ et bricoles diversesherbelin
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-05-06[ring] constructor for power was missing in the docbarras
2008-05-05Minor updates in the documentation of notations.glondu
2008-04-29Fix eauto still using delta when it shouldn't (should make CoRN compilemsozeau
2008-04-26Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour herbelin