aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-04-02Merge PR #9668: Consolidate credits and changelog information in a single place.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: vbgl
2019-04-02Merge PR #9875: [doc] Add a note about Dune support to the manual.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-02Document the Fast Name Printing option.Pierre-Marie Pédrot
2019-04-02Allow underscores as comments in numeral constants.Pierre Roux
The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)?
2019-04-02Update documentationPierre Roux
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-31Move content of COMPATIBILITY to Changes chapter.Théo Zimmermann
2019-03-31Move V8 CHANGES to Changes chapter.Théo Zimmermann
2019-03-31Move V7 CHANGES to History chapter.Théo Zimmermann
2019-03-31Change main sections in history chapter.Théo Zimmermann
2019-03-31Split credits chapter in two parts: history, and changelog in inverse ↵Théo Zimmermann
chronological order.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 18:12:53 +0000