Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #6480: Allow Prop as source for coercions | Maxime Dénès | 2018-03-09 |
|\ | |||
* \ | Merge PR #6895: [compat] Remove "Refolding Reduction" option. | Maxime Dénès | 2018-03-09 |
|\ \ | |||
| | * | added test for coercion from type | charguer | 2018-03-09 |
| | | | |||
| | * | allow Prop as source for coercions | charguer | 2018-03-09 |
| |/ |/| | |||
* | | Merge PR #6945: Fix error with univ binders on monomorphic records. | Maxime Dénès | 2018-03-09 |
|\ \ | |||
* \ \ | Merge PR #6155: Get rid of ' notation for Zpos in QArith | Maxime Dénès | 2018-03-09 |
|\ \ \ | |||
* \ \ \ | Merge PR #6747: Relax conversion of constructors according to the pCuIC model | Maxime Dénès | 2018-03-09 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6328: Fix #6313: lost goals in nested ltac in refine | Maxime Dénès | 2018-03-09 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values | Maxime Dénès | 2018-03-09 |
|\ \ \ \ \ \ | |||
| | * | | | | | More examples about shelve/given_up in tactic-in-terms. | Hugo Herbelin | 2018-03-08 |
| | | | | | | | |||
| | * | | | | | Proof engine: support for nesting tactic-in-term within other tactics. | Hugo Herbelin | 2018-03-08 |
| |/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Tactic-in-term can be called from within a tactic itself. We have to preserve the preexisting future_goals (if called from pretyping) and we have to inform of the existence of pending goals, using future_goals which is the only way to tell it in the absence of being part of an encapsulating proofview. This fixes #6313. Conversely, future goals, created by pretyping, can call ltac:(giveup) or ltac:(shelve), and this has to be remembered. So, we do it. | ||
* | | | | | | Merge PR #6522: Fix core hint database issue #6521 | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵ | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | wish #4129) | ||
| | | | | | | | * | [compat] Remove "Refolding Reduction" option. | Emilio Jesus Gallego Arias | 2018-03-08 |
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895. | ||
| | | | | | | * | Fix error with univ binders on monomorphic records. | Gaëtan Gilbert | 2018-03-08 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were declared twice for all records. Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an observable error for monomorphic records. | ||
| | | | * | | | | Fix SR breakage due to allowing fixpoints on non-rec values | Matthieu Sozeau | 2018-03-08 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work | ||
| | | | | * | | | Add test-suite file for cumulative constructors | Matthieu Sozeau | 2018-03-08 |
| | | | | | |/ | | | | | |/| | |||
* | | | | | | | Merge PR #6899: [compat] Remove "Standard Proposition Elimination" | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | | | |||
* | | | | | | | Merge PR #6582: Mangle auto-generated names | 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 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj` | 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 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | | | | An experimental 'Show Extraction' command (grant feature wish #4129) | Pierre Letouzey | 2018-03-06 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms. | ||
| | | | | * | | | | | | | | [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. | ||
| | | | | * | | | | | | | | 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 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | CHANGES and tests for with Definition @{univs} | Gaëtan Gilbert | 2018-03-05 |
| | | | | | | | | | | | | | | |||
| | | | * | | | | | | | | | | Sanitize universe declaration in Context (stop using a ref...) | Gaëtan Gilbert | 2018-03-05 |
| | | | |/ / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them. | ||
* | | | | | | | | | | | | | Merge PR #6855: Update headers following #6543. | Maxime Dénès | 2018-03-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | | | | [compat] Remove NOOP and alias deprecated options. | Emilio Jesus Gallego Arias | 2018-03-04 |
| | | | |/ / / / / / / / / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP. | ||
| | * / | | | | | | | | | | Remove deprecated options related to typeclasses. | Théo Zimmermann | 2018-03-04 |
| | |/ / / / / / / / / / | |||
| | | | * / / / / / / / | ssr: add Prenex Implicits for Some_inj to use it as a view | Anton Trunov | 2018-03-04 |
| | | |/ / / / / / / / | | |/| | | | | | | | | |||
* | | | | | | | | | | | Merge PR #935: Handling evars in the VM | Maxime Dénès | 2018-03-04 |
|\ \ \ \ \ \ \ \ \ \ \ | |_|/ / / / / / / / / |/| | | | | | | | | | | |||
* | | | | | | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5. | Maxime Dénès | 2018-03-04 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ↵ | Maxime Dénès | 2018-03-04 |
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | size. | ||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #915: Fix rewrite in * side conditions | Maxime Dénès | 2018-03-04 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | | | | Removing test for bug #2850. | Pierre-Marie Pédrot | 2018-03-03 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This test was actually checking that evar-containing terms were making the VM fail. Obviously this is not the case anymore, so the test is now invalid. | ||
| | | | * | | | | | | | | | | Adding a test file for evar handling in the VM. | Pierre-Marie Pédrot | 2018-03-03 |
| | | | | |_|_|_|/ / / / / | | | | |/| | | | | | | | | |||
| | | | | | | | * | | | | | [compat] Remove "Standard Proposition Elimination" | Emilio Jesus Gallego Arias | 2018-03-03 |
| | | | | |_|_|/ / / / / | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove the option "Standard Proposition Elimination" | ||
| | | * | | | | | | | | | Remove 8.5 compatibility support. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | | | | | |||
| | | * | | | | | | | | | Remove VOld compatibility flag. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | | | | | |||
| | | * | | | | | | | | | Turn warning for deprecated notations on. | Théo Zimmermann | 2018-03-02 |
| | | |/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fix new deprecation warnings in the standard library. | ||
| | * / / / / / / / / | Fix #6878: univ undefined for [with Definition] bad instance size. | Gaëtan Gilbert | 2018-03-01 |
| | |/ / / / / / / / | |||
| * / / / / / / / / | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | Hugo Herbelin | 2018-03-01 |
| |/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | Noticed by Sigurd Schneider. | ||
* / / / / / / / / | [test-suite] Add a basic test-case for `Load`. | Emilio Jesus Gallego Arias | 2018-02-28 |
|/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We test the 3 possible scenarios. A more complete test would also involved fake_ide. c.f. #6793 |