aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Program.tex
AgeCommit message (Expand)Author
2010-01-30Update CHANGES, add documentation for new commands/tactics and do a bitmsozeau
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-18Last changes in type class syntax: msozeau
2008-09-14A pass on documentation: msozeau
2008-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
2008-05-13- Fix bug related to indices of fixpoints.msozeau
2008-04-15Document CHANGES in setoid rewrite, move DefaultRelation tomsozeau
2008-04-01Add option to set the opacity of obligations to transparent, to be ablemsozeau
2008-03-23Fix examples in Program documentation and add comindexes for the variousmsozeau
2008-02-08New "Preterm [ of id ] " command to show the preterm before giving it tomsozeau
2008-01-05Standardisation du format des références croisées vers Figure, Section, Ch...herbelin
2007-10-24Doc updatemsozeau
2007-09-01A word on the measure and wf modifiersmsozeau
2007-08-26Add info on measure based defs.msozeau
2007-08-22Save IS NOT the same Defined ....msozeau
2007-08-08A better Program documentation. Include it in the generated stdlib doc.msozeau
2007-07-19Documentation of Program and its tactics, fix enormous interaction bug due to...msozeau
2007-01-31Fix typo.msozeau
2007-01-31Fix order of wf and measure arguments, patch Program doc.msozeau
2006-11-02Add doc on obligation solving commands.msozeau
2006-06-01Update Program/subtac documentation.msozeau
2006-04-07- Documentation of the Program tactics.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:11:10 +0000