aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
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-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-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
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-21Correction bug 1838 + doc modules.soubiran
2008-04-17documentation tactique gappafilliatr
2008-04-17Add almost empty Classes.tex for documentation of type classes.msozeau
2008-04-15Document CHANGES in setoid rewrite, move DefaultRelation tomsozeau
2008-04-15* added a subsection to explain the automatic declaration of schemes:vsiles
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
2008-04-15typovsiles
2008-04-14Update doc and remove another overloading of equiv_*.msozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-12Document the new setoid rewrite tactic, and fix a few things whilemsozeau
2008-04-03Chgts mineurs:herbelin
2008-04-01Add option to set the opacity of obligations to transparent, to be ablemsozeau
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
2008-03-23Fix examples in Program documentation and add comindexes for the variousmsozeau
2008-03-19migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...letouzey
2008-03-10Indexation de pose proof, et par la même occasion du nouveau specializeherbelin
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
2008-03-06repair for commit 10612 (due to grammar order, some syntaxes weren't working) letouzey
2008-03-01Rework on rich forms of rewriteletouzey
2008-02-09Fix the clrewrite tactic, change Relations.v to work on relations in Propmsozeau
2008-02-08Documentation of CHANGES and refman doc for the implicit argument bindermsozeau
2008-02-08New "Preterm [ of id ] " command to show the preterm before giving it tomsozeau
2008-02-06- Documentation des nouvelles options d'implicites (Set Strongly Strictherbelin
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau