aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-04-30Change entry from #9651.Théo Zimmermann
2019-04-30Change entry for #10014.Théo Zimmermann
2019-04-30Add number of commits, PRs and issues closed.Théo Zimmermann
2019-04-30Advertize continuous deployment of documentation.Théo Zimmermann
2019-04-30More review suggestions.Théo Zimmermann
2019-04-30Remove remaining references to CHANGES.md from the Recent changes chapter.Théo Zimmermann
2019-04-30Remove misplaced CHANGES entry and fix links formatting.Théo Zimmermann
PR #8187 misplaced its CHANGES entry. We remove it in this commit instead of moving it to the right place because it is reverted in #9987.
2019-04-30Finish adding authors and links to PRs.Théo Zimmermann
2019-04-30Change entry for #9906.Théo Zimmermann
2019-04-30Split changes between main changes and other changes (no repetition).Théo Zimmermann
Add more links to PRs and credits of authors.
2019-04-30Remove 8.10 entries from CHANGES file.Théo Zimmermann
2019-04-30First fixing pass, and experiment with dune-style PR number and author listing.Théo Zimmermann
2019-04-30Apply suggestions from code review Théo Zimmermann
Mainly markup fixes by Theo Co-Authored-By: mattam82 <matthieu.sozeau@inria.fr>
2019-04-30Credits for 8.10Matthieu Sozeau
2019-04-29Merge PR #9987: Fix #9180 by reverting #9249 and #8187Emilio Jesus Gallego Arias
Reviewed-by: maximedenes
2019-04-29Merge PR #9651: [ssr] Add tactics under and overCyril Cohen
Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: erikmd Ack-by: gares Ack-by: jfehrle
2019-04-29Merge PR #10011: [refman] Fix typo.Vincent Laporte
Reviewed-by: vbgl
2019-04-29Merge PR #10018: Document unshelve (#3225)Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-29Revert #8187Vincent Laporte
2019-04-29Document unshelve (#3225)Paolo G. Giarrusso
I believe this is the appropriate place for users to read about this, even tho `unshelve` is technically a tactical. This example was explicitly requested in #3225 and is commonly used in both Iris (and was documented in the changelog at the time).
2019-04-28Merge PR #9605: [coq_makefile] Enforce warn_error for plugins.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares
2019-04-27Minor doc improvement.Théo Zimmermann
2019-04-27[refman] Fix typo.Théo Zimmermann
Noticed by Maxime Dénès.
2019-04-24Merge PR #9988: [refman] Properly define token regexp.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-04-24[refman] Fix a quoting problem.Théo Zimmermann
2019-04-24[refman] Properly define token regexp.Théo Zimmermann
2019-04-24[coq_makefile] Enforce warn_error for plugins.Emilio Jesus Gallego Arias
The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974
2019-04-23[ssr] under: optimization of the tactic for (under eq_bigl => *)Erik Martin-Dorel
so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|]. Also: replace "by over." in the doc example with "over."
2019-04-23[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notationsErik Martin-Dorel
as suggested by @gares, and: * Rename some Under_* terms for better uniformity; * Update & Improve minor details in the documentation.
2019-04-23[doc] ssr_under: a few improvementsEnrico Tassi
2019-04-23[ssr] under: Fix the defective form ("=> [*|*]" implied) and its docErik Martin-Dorel
* Add tests accordingly.
2019-04-23[ssr] under: Fix and extend the documentationErik Martin-Dorel
2019-04-23[ssr] new syntax for the under tacticEnrico Tassi
2019-04-23[ssr] under: Add doc for {under, over} & Add entry in CHANGES.mdErik Martin-Dorel
* For better uniformity, replace "intro-pattern" with "intro pattern" in the ssr doc.
2019-04-17Merge PR #9876: Command-line setters for optionsEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares
2019-04-16Update and fix documentation of Program Fixpoint with measureMaxime Dénès
2019-04-16Command-line setters for optionsGaëtan Gilbert
TODO coqproject handling (for now it can be done through -arg I guess)
2019-04-10Improve SProp error message to mention the Allow StrictProp flag.Théo Zimmermann
And document the error message.
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01
2019-04-03Merge PR #9078: Provide a faster bound name generation algorithm through a flagVincent Laporte
Ack-by: jfehrle Ack-by: ppedrot Reviewed-by: vbgl
2019-04-03Minor correction to numeral notations docJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 07:40:02 +0000