Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #6743: Add notation {x & P} for sigT | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6927: Add some missing flushes in configure. | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6909: Deprecate Focus and Unfocus | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6899: [compat] Remove "Standard Proposition Elimination" | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6881: [windows] support -addon in build script | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | Merge PR #6582: Mangle auto-generated names | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6933: Standard headers for C and Python. | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6934: Warn when using “Require” in a section | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6924: Clean-up remove always false useeager argument. | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6902: [compat] Remove "Discriminate Introduction" | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6903: [compat] Remove "Shrink Abstract" | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634) | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | | | | | | | | * | | [toplevel] Respect COQ_COLORS environment variable | 2018-03-07 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | | | | | gitlab: install num for all jobs | 2018-03-07 | ||
| | | | | | | | | | | | | | | | | | | | | | | * | | | | [checker] Printer cleanup. | 2018-03-07 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | | | | | | | | | Use a proper warning when a summary is captured out of module scope. | 2018-03-07 | ||
| | | | | * | | | | | | | | | | | | | | | | | | | | | [vernac] Warn when using “Require” in a section | 2018-03-07 | ||
| | | | | * | | | | | | | | | | | | | | | | | | | | | [stdlib] Do not use “Require” inside sections | 2018-03-07 | ||
| |_|_|_|/ / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | * | | | | | Add empty compat file for Coq 8.8 | 2018-03-07 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6744: Add String.concat | 2018-03-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6932: [stdlib] Do not use deprecated notations | 2018-03-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6905: Fix make ml-doc | 2018-03-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj` | 2018-03-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6922: Remove outdated information regarding the FAQ. | 2018-03-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6374: [toplevel] Modify printing goal strategy. | 2018-03-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6790: Allow universe declarations for [with Definition]. | 2018-03-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...) | 2018-03-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | | Add CHANGES and man entry for coqdep learning _CoqProject. | 2018-03-06 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | | Closes #6830: coqdep reads options and files from _CoqProject. | 2018-03-06 | ||
| | | | | | | | | | | | | | | | | | | | | | | * | | | | | | | | An experimental 'Show Extraction' command (grant feature wish #4129) | 2018-03-06 | ||
| | | | | | | | | | | | | | | | | | | | | | | * | | | | | | | | Extraction: switch to EConstr.t as the central type to extract from. | 2018-03-06 | ||
| | | | | | | | | | | | | | | | | | | | | * | | | | | | | | | | romega: get rid of EConstr.Unsafe | 2018-03-06 | ||
| | | | | | | | | | | | | | | | | | | | | | |/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | |/| | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | * | | | | | | | | | | document -profile in dev/doc/setup.txt | 2018-03-06 | ||
| | | | | | | | | | | | | * | | | | | | | | | | | | | | | | | Standard headers for C and Python. | 2018-03-06 | ||
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | | | | | | | | | | | | | [stdlib] Do not use deprecated notations | 2018-03-06 | ||
| |_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | * | | | | | | | | | | | | Add some missing flushes in configure. | 2018-03-06 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | | | | | | | | | | | | Hack to make bignum build on windows | 2018-03-06 | ||
| | | | | | | | | | | | | * | | | | | | | | | | | | | | build: win: turn off build/installation of gnu Make | 2018-03-06 | ||
| | | | | | | | | | | * | | | | | | | | | | | | | | | | Clean-up remove always false useeager argument. | 2018-03-06 | ||
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | | | | | | | | | | | | | Remove outdated information regarding the FAQ. | 2018-03-06 | ||
| |_|_|/ / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | | | Rename some universe minimizing "normalize" functions to "minimize" | 2018-03-06 | ||
| | | | | | | | | | | | | | | | | * | | | | | | | | Deprecate UState aliases in Evd. | 2018-03-06 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6917: Fix failing packaging job. | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | | | | | | | | | | [compat] Remove "Discriminate Introduction" | 2018-03-06 | ||
| |_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | | | | | | | | | [compat] Remove "Shrink Abstract" | 2018-03-06 | ||
| |_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ... | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6795: [ssreflect] Export parsing witnesses in mli file. | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | | | | | | | | | | ssr: use `apply_type ~typecheck:true` everywhere (fix #6634) | 2018-03-06 | ||
* | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6896: [compat] Remove NOOP deprecated options. | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6824: Remove deprecated options related to typeclasses. | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |