aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-04-02Merge PR #9875: [doc] Add a note about Dune support to the manual.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-01Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and ↵Vincent Laporte
#9615) Reviewed-by: Zimmi48 Ack-by: fajb Reviewed-by: vbgl
2019-04-01[doc] Add a note about Dune support to the manual.Emilio Jesus Gallego Arias
2019-04-01Update numeral notation printing docJason Gross
Fixes #9844
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-30[Manual] TypoVincent Laporte
2019-03-29typo in ring.rstthery
2019-03-28Merge PR #9129: [proof] Removal of imperative state ; interpretation layers ↵Maxime Dénès
only. Ack-by: SkySkimmer Reviewed-by: aspiwack Ack-by: ejgallego Ack-by: gares Ack-by: herbelin Reviewed-by: mattam82 Ack-by: maximedenes
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Ack-by: pi8027
2019-03-27Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.Jim Fehrle
2019-03-27[doc] [abstract] Document a bit some problems with abstract.Emilio Jesus Gallego Arias
2019-03-27Deprecate `Refine Instance Mode` optionMaxime Dénès
This is in view of the 8.10 release, after which we will remove the option and the `VtUnknown` classification.
2019-03-26Merge PR #9829: [Vernacular] Deprecate the “Show Script” commandEnrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares # Conflicts: # CHANGES.md
2019-03-26Fix syntax of Typeclasses eauto := in reference manual.Théo Zimmermann
2019-03-25[Vernacular] Deprecate the “Show Script” commandVincent Laporte
Fixes #8320
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
This option made the Coercions command follow non-standard scoping rules (effect on `Require` rather than `Import`). It was already marked for deletion in 8.8.
2019-03-25Fix indentationGan Shen
2019-03-25Update doc/sphinx/language/gallina-extensions.rstThéo Zimmermann
Co-Authored-By: gshen42 <gan.shen@outlook.com>
2019-03-24Fix typoGan Shen
2019-03-22Merge PR #8560: Unicode bindings for CoqIDE that works out of the boxPierre-Marie Pédrot
Reviewed-by: Zimmi48 Ack-by: charguer Reviewed-by: gares Reviewed-by: ppedrot
2019-03-21Merge PR #9789: [Manual] Improve documentation on Section, Variable, ContextThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: jfehrle
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-18[Manual] Parametrize -> ParametErizeLysxia
- Refine some `@term` into `@type`
2019-03-18Update doc and changesKazuhiko Sakaguchi
2019-03-18[Manual] Move command Context after Let, and more polishingLysxia
- Refine some `@term` into `@type`
2019-03-18fix documentation issues, and add entry to change logcharguer
2019-03-18polishing documentation for coqide bindings, following @Zimmi48 commentscharguer
2019-03-18final polishing for coqide bindingscharguer
2019-03-18documentation for unicode bindingscharguer
2019-03-17[Manual] Move doc on Let into Section mechanism, and more polishingLysxia
- Put "Section mechanism" example earlier
2019-03-17[Manual] Gather section-specific commands in Section documentation (fix #9704)Lysxia
2019-03-17[Manual] Improve chapter Type classes, and add mention of Context under VariableLysxia
- More consistent code indentation - Nest command variants properly - Make `Context` explanation a bit less terse, with more links - Typesetting bits, add some :cmd: links
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-13[refman] Fix Sphinx-translation regression in Arguments command.Théo Zimmermann
2019-03-13[refman] Remove warning silencing by fixing the underlying issue.Théo Zimmermann
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-03-12[refman] Add 'warn' option to coqtop directive.Théo Zimmermann
Fix semantic conflict between #9389 and #9654.
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug
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-28Add DOIs.Théo Zimmermann
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
2019-02-28Move content of README-V1-V5 to Credits chapter.Théo Zimmermann
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
This is intended to be separate from handling of implicit binders. The remaining uses of declare_manual_implicits satisfy a lot of assertions, giving the possibility of simplifying the interface in the future. Two disabled warnings are added for things that currently pass silently. Currently only Mtac passes non-maximal implicits to declare_manual_implicits with the force-usage flag set. When implicit arguments don't have to be named, should move Mtac over to set_implicits.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 16:17:33 +0000