Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Update checker to reflect rule on constructors of polymorphic inductive types | Matthieu Sozeau | 2018-03-08 |
| | |||
* | Relax conversion of constructors according to the pCuIC model | Matthieu Sozeau | 2018-03-08 |
| | | | | | | - Nothing to check in conversion as they have a common supertype by typing. - In inference, enforce that one is lower than the other. | ||
* | Merge PR #6582: Mangle auto-generated names | Maxime Dénès | 2018-03-08 |
|\ | |||
* \ | Merge PR #6933: Standard headers for C and Python. | Maxime Dénès | 2018-03-08 |
|\ \ | |||
* \ \ | Merge PR #6934: Warn when using “Require” in a section | Maxime Dénès | 2018-03-08 |
|\ \ \ | |||
* \ \ \ | Merge PR #6924: Clean-up remove always false useeager argument. | Maxime Dénès | 2018-03-08 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6902: [compat] Remove "Discriminate Introduction" | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6903: [compat] Remove "Shrink Abstract" | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634) | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ \ | |||
| | | | | * | | | Use a proper warning when a summary is captured out of module scope. | Vincent Laporte | 2018-03-07 |
| | | | | | | | | |||
| | | | | * | | | [vernac] Warn when using “Require” in a section | Vincent Laporte | 2018-03-07 |
| | | | | | | | | |||
| | | | | * | | | [stdlib] Do not use “Require” inside sections | Vincent Laporte | 2018-03-07 |
| |_|_|_|/ / / |/| | | | | | | |||
* | | | | | | | Merge PR #6744: Add String.concat | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6932: [stdlib] Do not use deprecated notations | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6905: Fix make ml-doc | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj` | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6922: Remove outdated information regarding the FAQ. | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6374: [toplevel] Modify printing goal strategy. | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6790: Allow universe declarations for [with Definition]. | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...) | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | * | | Standard headers for C and Python. | Maxime Dénès | 2018-03-06 |
| |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | |||
| | | | | | | * | | | | | | | [stdlib] Do not use deprecated notations | Vincent Laporte | 2018-03-06 |
| |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | |||
| | | | | | | | | | | * | | Clean-up remove always false useeager argument. | Théo Zimmermann | 2018-03-06 |
| |_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | |||
| | | | * | | | | | | | | Remove outdated information regarding the FAQ. | Théo Zimmermann | 2018-03-06 |
| |_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The FAQ is not part of the Coq sources anymore. | ||
* | | | | | | | | | | | Merge PR #6917: Fix failing packaging job. | Maxime Dénès | 2018-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | * | | [compat] Remove "Discriminate Introduction" | Emilio Jesus Gallego Arias | 2018-03-06 |
| |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we the option "Discriminate Introduction". | ||
| | | | | | | | | * | | [compat] Remove "Shrink Abstract" | Emilio Jesus Gallego Arias | 2018-03-06 |
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we the option "Shrink Abstract". | ||
* | | | | | | | | | | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵ | Maxime Dénès | 2018-03-06 |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | a record. | ||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6795: [ssreflect] Export parsing witnesses in mli file. | Maxime Dénès | 2018-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | * | | ssr: use `apply_type ~typecheck:true` everywhere (fix #6634) | Enrico Tassi | 2018-03-06 |
| | | | | | | | | | | | | |||
* | | | | | | | | | | | | Merge PR #6896: [compat] Remove NOOP deprecated options. | Maxime Dénès | 2018-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6824: Remove deprecated options related to typeclasses. | Maxime Dénès | 2018-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6900: [compat] Remove "Tactic Pattern Unification" | Maxime Dénès | 2018-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6898: [compat] Remove "Intuition Iff Unfolding" | Maxime Dénès | 2018-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6901: [compat] Remove "Injection L2R Pattern Order" | Maxime Dénès | 2018-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | | | [toplevel] Modify printing goal strategy. | Emilio Jesus Gallego Arias | 2018-03-05 |
| |_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of using a command-analysis heuristic, coqtop will now print goals if the goal has changed. We use a fast goal comparison heuristic, but a more refined strategy would be possible. This brings some [IMHO very welcome] change to PG and `-emacs`, which will now disable the printing of goals. Now, instead of playing with `Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show` command whenever it wishes to redisplay the goals. This change will break PG, so we need to carefully coordinate this PR with PG upstream (see ProofGeneral/PG#212). Some interesting further things to do: - Detect changes in nested proofs. - Uncouple the silent flag from "print goals". | ||
| | | | | | | | * | | | | | | | Fix failing packaging job. | Théo Zimmermann | 2018-03-05 |
| |_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | gtksourceview depends transitively on py2cairo which was updated in Homebrew to depend explicitly on python2 (see Homebrew/homebrew-core#24714): this makes the python3 install step impossible. We also remove the libxml2 install step which was failing in a non-fatal way. | ||
| | | | | | | | | | | * | | | Remove NOPLUGINDOCS option | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Add empty description for @raise statements to satisfy ocamldoc | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Escape curly braces in ocamldoc comment | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Separate vim/emacs fold markers from ocamldoc comments | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ocamldoc chokes on the markers {{{ and }}} because { and } are part of its syntax | ||
| | | | | | | | | | | * | | | Build docs for plugins by default, add NOPLUGINDOCS flag to disable | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Change non-documentation comment from ocamldoc style | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Fix formatting of some ocamldoc comments to reduce warnings | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Replace invalid tag @raises in ocamldoc comments with @raise | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Remove non-existent dependency | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Tweak comments to fix ocamldoc errors | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Tidy up ml-doc outut, give it a separate output directory | mrmr1993 | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | Use computed deps to generate ml-doc and use implicit mli-doc deps | mrmr1993 | 2018-03-05 |
| |_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | |||
| | | | | | | | | * | | | | CHANGES and tests for with Definition @{univs} | Gaëtan Gilbert | 2018-03-05 |
| | | | | | | | | | | | | |