| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-04-29 | Document 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-28 | Merge PR #9605: [coq_makefile] Enforce warn_error for plugins. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares | |||
| 2019-04-27 | Minor doc improvement. | Théo Zimmermann | |
| 2019-04-27 | [refman] Fix typo. | Théo Zimmermann | |
| Noticed by Maxime Dénès. | |||
| 2019-04-24 | Merge 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[ _ ] notations | Erik 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 improvements | Enrico Tassi | |
| 2019-04-23 | [ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc | Erik Martin-Dorel | |
| * Add tests accordingly. | |||
| 2019-04-23 | [ssr] under: Fix and extend the documentation | Erik Martin-Dorel | |
| 2019-04-23 | [ssr] new syntax for the under tactic | Enrico Tassi | |
| 2019-04-23 | [ssr] under: Add doc for {under, over} & Add entry in CHANGES.md | Erik Martin-Dorel | |
| * For better uniformity, replace "intro-pattern" with "intro pattern" in the ssr doc. | |||
| 2019-04-21 | Remove duplicate copy of _warn_if_duplicate_name. | Jim Fehrle | |
| 2019-04-17 | Merge PR #9876: Command-line setters for options | Emilio Jesus Gallego Arias | |
| Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares | |||
| 2019-04-16 | Update and fix documentation of Program Fixpoint with measure | Maxime Dénès | |
| 2019-04-16 | Command-line setters for options | Gaëtan Gilbert | |
| TODO coqproject handling (for now it can be done through -arg I guess) | |||
| 2019-04-10 | Improve SProp error message to mention the Allow StrictProp flag. | Théo Zimmermann | |
| And document the error message. | |||
| 2019-04-05 | Merge 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-03 | Merge PR #9078: Provide a faster bound name generation algorithm through a flag | Vincent Laporte | |
| Ack-by: jfehrle Ack-by: ppedrot Reviewed-by: vbgl | |||
| 2019-04-03 | Merge PR #9896: Minor correction to numeral notations doc | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-04-03 | Merge PR #8638: Remove -compat 8.7 | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: jfehrle Ack-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-04-03 | Minor correction to numeral notations doc | Jason Gross | |
| 2019-04-02 | Merge PR #9668: Consolidate credits and changelog information in a single place. | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel Reviewed-by: vbgl | |||
| 2019-04-02 | Remove -compat 8.7 | Jason Gross | |
| This removes various compatibility notations. Closes #8374 This commit was mostly created by running `./dev/tools/update-compat.py --release`. There's a bit of manual spacing adjustment around all of the removed compatibility notations, and some test-suite updates were done manually. The update to CHANGES.md was manual. | |||
| 2019-04-02 | Merge PR #9875: [doc] Add a note about Dune support to the manual. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-04-02 | Document the Fast Name Printing option. | Pierre-Marie Pédrot | |
| 2019-04-02 | Allow 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-02 | Update documentation | Pierre Roux | |
| 2019-04-01 | Merge 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-01 | Update numeral notation printing doc | Jason Gross | |
| Fixes #9844 | |||
| 2019-04-01 | Several improvements and fixes of Lia | Fré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-31 | Move content of COMPATIBILITY to Changes chapter. | Théo Zimmermann | |
| 2019-03-31 | Move V8 CHANGES to Changes chapter. | Théo Zimmermann | |
| 2019-03-31 | Move V7 CHANGES to History chapter. | Théo Zimmermann | |
| 2019-03-31 | Change main sections in history chapter. | Théo Zimmermann | |
| 2019-03-31 | Split credits chapter in two parts: history, and changelog in inverse ↵ | Théo Zimmermann | |
| chronological order. | |||
| 2019-03-30 | [Manual] Typo | Vincent Laporte | |
| 2019-03-29 | typo in ring.rst | thery | |
| 2019-03-28 | Merge 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-28 | Merge PR #9743: Relax the ambiguous path condition of coercion | Enrico Tassi | |
| Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Ack-by: pi8027 | |||
| 2019-03-27 | Merge 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-27 | [plugin tutorial] Adapt to removal of imperative state. | Emilio Jesus Gallego Arias | |
| 2019-03-27 | Deprecate `Refine Instance Mode` option | Maxime 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-26 | Merge PR #9829: [Vernacular] Deprecate the “Show Script” command | Enrico Tassi | |
| Reviewed-by: Zimmi48 Reviewed-by: gares # Conflicts: # CHANGES.md | |||
| 2019-03-26 | Fix syntax of Typeclasses eauto := in reference manual. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |