aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Program.tex
AgeCommit message (Expand)Author
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-07-11Sync the manual with the deprecation warnings.Théo Zimmermann
2016-06-29Fixes in documentation.Matthieu Sozeau
2016-06-29Program: cleanup in cases, add optionsMatthieu Sozeau
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-09-08Documenting the new behaviour of the Shrink Obligations flag.Pierre-Marie Pédrot
2015-07-30Fix some broken Coq scripts in the documentation.Guillaume Melquiond
2015-03-31Fix various typos in documentationMatěj Grabovský
2015-02-17Separate index for vernacular options.Maxime Dénès
2013-06-06Document changes and add missing documentation for Program options.msozeau
2012-09-05Obsolete syntax in documentation of Solve Obligation commands.ppedrot
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-10-07Remove 'status' of Program and explain the :> better, as well as referencing ...msozeau
2011-09-01Bug 2583: Update of the syntax of terms in the reference manualpboutill
2010-06-08Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".herbelin
2010-03-31Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]msozeau
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