aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Program.tex
Commit message (Expand)AuthorAge
* Fixes in documentation.Gravatar Matthieu Sozeau2016-06-29
* Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* | Documenting the new behaviour of the Shrink Obligations flag.Gravatar Pierre-Marie Pédrot2015-09-08
|/
* Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Document changes and add missing documentation for Program options.Gravatar msozeau2013-06-06
* Obsolete syntax in documentation of Solve Obligation commands.Gravatar ppedrot2012-09-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Remove 'status' of Program and explain the :> better, as well as referencing ...Gravatar msozeau2011-10-07
* Bug 2583: Update of the syntax of terms in the reference manualGravatar pboutill2011-09-01
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]Gravatar msozeau2010-03-31
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* A pass on documentation: Gravatar msozeau2008-09-14
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* - Fix bug related to indices of fixpoints.Gravatar msozeau2008-05-13
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
* Add option to set the opacity of obligations to transparent, to be ableGravatar msozeau2008-04-01
* Fix examples in Program documentation and add comindexes for the variousGravatar msozeau2008-03-23
* New "Preterm [ of id ] " command to show the preterm before giving it toGravatar msozeau2008-02-08
* Standardisation du format des références croisées vers Figure, Section, Ch...Gravatar herbelin2008-01-05
* Doc updateGravatar msozeau2007-10-24
* A word on the measure and wf modifiersGravatar msozeau2007-09-01
* Add info on measure based defs.Gravatar msozeau2007-08-26
* Save IS NOT the same Defined ....Gravatar msozeau2007-08-22
* A better Program documentation. Include it in the generated stdlib doc.Gravatar msozeau2007-08-08
* Documentation of Program and its tactics, fix enormous interaction bug due to...Gravatar msozeau2007-07-19
* Fix typo.Gravatar msozeau2007-01-31
* Fix order of wf and measure arguments, patch Program doc.Gravatar msozeau2007-01-31
* Add doc on obligation solving commands.Gravatar msozeau2006-11-02
* Update Program/subtac documentation.Gravatar msozeau2006-06-01
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07