Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials | 2018-03-08 | |
|\ | |||
* \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish... | 2018-03-08 | |
|\ \ | |||
* \ \ | Merge PR #6899: [compat] Remove "Standard Proposition Elimination" | 2018-03-08 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6582: Mangle auto-generated names | 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 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj` | 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 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | An experimental 'Show Extraction' command (grant feature wish #4129) | 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 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | 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 | |
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |||
| | | | | * | | | | | | CHANGES and tests for with Definition @{univs} | 2018-03-05 | |
| | | | * | | | | | | | Sanitize universe declaration in Context (stop using a ref...) | 2018-03-05 | |
| | | | |/ / / / / / | |||
* | | | | | | | | | | Merge PR #6855: Update headers following #6543. | 2018-03-05 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | [compat] Remove NOOP and alias deprecated options. | 2018-03-04 | |
| | | | |/ / / / / / | | | |/| | | | | | | |||
| | * / | | | | | | | Remove deprecated options related to typeclasses. | 2018-03-04 | |
| | |/ / / / / / / | |||
| | | | * / / / / | ssr: add Prenex Implicits for Some_inj to use it as a view | 2018-03-04 | |
| | | |/ / / / / | | |/| | | | | | |||
* | | | | | | | | Merge PR #935: Handling evars in the VM | 2018-03-04 | |
|\ \ \ \ \ \ \ \ | |_|/ / / / / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5. | 2018-03-04 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ... | 2018-03-04 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #915: Fix rewrite in * side conditions | 2018-03-04 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | Removing test for bug #2850. | 2018-03-03 | |
| | | | * | | | | | | | Adding a test file for evar handling in the VM. | 2018-03-03 | |
| | | | | |_|_|_|/ / | | | | |/| | | | | | |||
| | | | | | | | * | | [compat] Remove "Standard Proposition Elimination" | 2018-03-03 | |
| | | | | |_|_|/ / | | | | |/| | | | | |||
| | | * | | | | | | Remove 8.5 compatibility support. | 2018-03-02 | |
| | | * | | | | | | Remove VOld compatibility flag. | 2018-03-02 | |
| | | * | | | | | | Turn warning for deprecated notations on. | 2018-03-02 | |
| | | |/ / / / / | |||
| | * / / / / / | Fix #6878: univ undefined for [with Definition] bad instance size. | 2018-03-01 | |
| | |/ / / / / | |||
| * / / / / / | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | 2018-03-01 | |
| |/ / / / / | |||
* / / / / / | [test-suite] Add a basic test-case for `Load`. | 2018-02-28 | |
|/ / / / / | |||
* | | | | | Merge PR #6756: Fix issue with spurious timing test failures | 2018-02-28 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit... | 2018-02-28 | |
|\ \ \ \ \ \ | |||
| | | * | | | | Update headers following #6543. | 2018-02-27 | |
| |_|/ / / / |/| | | | | | |||
| | * | | | | [test-suite] Move sed scripts into bash arrays | 2018-02-24 | |
* | | | | | | Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism). | 2018-02-24 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6599: Decimals in prelude | 2018-02-24 | |
|\ \ \ \ \ \ \ | |||
| | | * | | | | | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion). | 2018-02-23 | |
| |_|/ / / / / |/| | | | | | | |||
| | | | | | * | Adding mention of shelved/given-up status in "Show Existentials". | 2018-02-22 | |
| |_|_|_|_|/ |/| | | | | | |||
* | | | | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred` | 2018-02-21 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585) | 2018-02-21 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the... | 2018-02-21 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6740: Adding a sanity check on inductive variance subtyping. | 2018-02-21 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | Update SearchPattern.out for numeral notations | 2018-02-20 | |
| |_|_|_|/ / / / / |/| | | | | | | | | |||
| | | | | * | | | | Fixes bug #6774 (anomaly with ill-typed template polymorphism). | 2018-02-20 | |
| |_|_|_|/ / / / |/| | | | | | | | |||
| | | * | | | | | Adding a test for wish #5532. | 2018-02-20 | |
| | | * | | | | | Trying a hack to support {'pat|P} without breaking compatibility. | 2018-02-20 |