aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2019-04-02Document the Fast Name Printing option.Pierre-Marie Pédrot
2019-04-01Several improvements and fixes of LiaFrédéric Besson
- Improved reification for Micromega (support for #8764) - Fixes #9268: Do not take universes into account in lia reification Improve #9291 by threading the evar_map during reification. Universes are unified. - Remove (potentially cyclic) dependency over lra for Rle_abs - Towards a complete simplex-based lia fixes #9615 Lia is now exclusively using cutting plane proofs. For this to always work, all the variables need to be positive. Therefore, lia is pre-processing the goal for each variable x it introduces the constraints x = y - z , y>=0 , z >= 0 for some fresh variable y and z. For scalability, nia is currently NOT performing this pre-processing. - Lia is using the FSet library manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4 to work around a "leaked" hint breaking compatibility of eauto
2019-03-27[doc] [abstract] Document a bit some problems with abstract.Emilio Jesus Gallego Arias
2019-03-25[Vernacular] Deprecate the “Show Script” commandVincent Laporte
Fixes #8320
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jfehrle
2019-03-10Merge PR #9654: [sphinx] Add warn option to coqtop directive.Clément Pit-Claudel
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: vbgl Reviewed-by: cpitclaudel
2019-03-08[sphinx] Fix typo in local application of tacticshawnzug
2019-03-07Merge PR #9133: Move README-V1-V5 to credits chapterClément Pit-Claudel
Reviewed-by: cpitclaudel
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-03-01[doc] ssr: Fix the documentation of `by [tacs]`Erik Martin-Dorel
Closes coq/coq#9669
2019-02-28Move content of README-V1-V5 to Credits chapter.Théo Zimmermann
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
By default Coq warnings are made fatal when building the manual. If you want to show a command resulting in a warning, use the warn option. Preexisting warnings are either fixed or marked as expected.
2019-02-25[Manual] Refactor documentation of internal registration commandsVincent Laporte
2019-02-25[Manual] Document primitive integersVincent Laporte
2019-02-25[Manual] Document the “Primitive” commandVincent Laporte
2019-02-25[Manual] Document “Register Inline”Vincent Laporte
2019-02-25[Manual] Document “Register” to kernel namespaceVincent Laporte
2019-02-19[sphinx] Refactor handling of options for coqtop directive.Théo Zimmermann
Make it mandatory to give exactly one display option.
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
This uses a new coqtop-only option "Coqtop Exit On Error", not sure where to put the doc for it. It being an option means we can locally turn it off (.. coqtop:: fail).
2019-02-18Fix last nested lemma failure.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 23:06:09 +0000