aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2019-02-14Merge PR #9571: Document the now_show tactic.Clément Pit-Claudel
Ack-by: Zimmi48 Reviewed-by: cpitclaudel
2019-02-14Document the now_show tactic.Théo Zimmermann
It was used in the standard library and the test-suite but undocumented so far.
2019-02-14[Manual] Clean examples for `apply`Vincent Laporte
2019-02-14[Manual] Don’t use `Undo` in ssreflect examplesVincent Laporte
2019-02-14[Manual] Clean examples about `inversion` tacticVincent Laporte
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
Ack-by: Zimmi48
2019-02-12Fix failing coqtops in tactics.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ssreflect-proof-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ltac.rstGaëtan Gilbert
2019-02-12Improve the documentation of auto.Théo Zimmermann
In particular, mention that auto does not use full-blown apply.
2019-02-06Document the possibility of declaring a Ltac name_goal.Théo Zimmermann
2019-02-05Documenting the Ltac Backtrace flag.Pierre-Marie Pédrot
2019-02-05Add advice and an example to the documentation of fold.Théo Zimmermann
2019-01-28Surround "assumption" with :tacn:`` in tactics.rstRyan Scott
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: gares Reviewed-by: maximedenes
2019-01-24Merge PR #9384: Improve the note in the beginning of the Ltac chapter.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
Ack-by: Zimmi48 Ack-by: anton-trunov Ack-by: jfehrle
2019-01-24[doc] warn that (automatic) clears can result in errorsEnrico Tassi
2019-01-24[doc] more precise description of when automatic clears are triggeredEnrico Tassi
2019-01-24[doc] explain how to avoid automatic clearsEnrico Tassi
2019-01-23Move and rewrite documentation for intro patterns that was underJim Fehrle
the intros tactic to its own subsection. Add grammar and examples.
2019-01-23Fix the information of the level of ; vs ; [ ]Théo Zimmermann
2019-01-23Improve the note in the beginning of the Ltac chapter.Théo Zimmermann
In particular, add an example to illustrate the associativity of ;
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2019-01-22clarify when an ident is added to the clear switchEnrico Tassi
2019-01-22Apply suggestions from code reviewThéo Zimmermann
Co-Authored-By: gares <gares@fettunta.org>
2019-01-21ring and field simplify can take no argumentsthery
2019-01-21[ssr] better structure the ipats docEnrico Tassi
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
This is for consistency with "rewrite {x..} y"
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
2018-12-19[doc] typoEnrico Tassi
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
This commit implements the following intro patterns: Temporary "=> +" "move=> + stuff" ==== "move=> tmp stuff; move: tmp" It preserves the original name. "=>" can be chained to force generalization as in "move=> + y + => x z" Tactics as views "=> /ltac:(tactic)" Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo". Limited to views on the right of "=>", views that decorate a tactic as move or case are not supported to be tactics. Dependent "=> >H" move=> >H ===== move=> ???? H, with enough ? to name H the first non-dependent assumption (LHS of the first arrow). TC isntances are skipped. Block intro "=> [^ H] [^~ H]" after "case" or "elim" or "elim/v" it introduces in one go all new assumptions coming from the eliminations. The names are picked from the inductive type declaration or the elimination principle "v" in "elim/v" and are appended/prepended the seed "H" The implementation makes crucial use of the goal_with_state feature of the tactic monad. For example + schedules a generalization to be performed at the end of the intro pattern and [^ .. ] reads the name seeds from the state (that is filled in by case and elim).
2018-12-14Fix the SSReflect chapter regarding objects without bodies.Théo Zimmermann
2018-12-11Add missing formatting.Théo Zimmermann
2018-12-11Document the deprecation of hint declaration withou database in refman.Théo Zimmermann
Follow-up of #8987.
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
Also remove a few undocumented settings
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try ↵Théo Zimmermann
to fix all misuses.
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter.
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-06Improve rendering of the credits.Guillaume Melquiond
This mostly fixes text that was italicized instead of teletyped. When possible, tactic names have been made to point to their documentation. Also, the date of the 8.9 release has been proactively changed to November.
2018-10-24[Manual] Prevent an irrelevant warning to show upVincent Laporte
2018-10-24[Manual] Avoid using deprecated “Focus”Vincent Laporte
2018-10-24[Manual] Fix rendering of an exampleVincent Laporte
2018-10-24[Manual] TypoVincent Laporte
2018-10-24[Manual] Fix an exampleVincent Laporte
The `Undo` command is not reliable.
2018-10-24[Manual] Fix layout of a listVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-10 20:44:46 +0000