Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fixes #7195 (missing freshness condition in Ltac pattern-matching names). | Hugo Herbelin | 2018-04-08 |
| | | | | | | | | | | We ensure that all original names in a spine of matched nested binders are distinct. Note: This enforces that two binders with same internal names are kept disjoint but this does not enforce that we shall respect names exactly as they are printed. Only the original prefix of the internal names are preserved, not their "0" or "1" etc. suffix. | ||
* | Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092) | Pierre-Marie Pédrot | 2018-04-01 |
|\ | |||
* | | Change Implicit Arguments to Arguments in test-suite | Jasper Hugunin | 2018-03-30 |
| | | |||
* | | Fix #6631: Derive Plugin gives "Anomaly: more than one statement". | Pierre-Marie Pédrot | 2018-03-29 |
| | | | | | | | | | | | | We use a lower level function that accesses the proof without raising an anomaly. This is a direct candidate for backport, so I used a V82 API but eventually this API should be cleaned up. | ||
| * | Supporting fix/cofix in Ltac pattern-matching (wish #7092). | Hugo Herbelin | 2018-03-28 |
|/ | | | | | This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern. | ||
* | Allow using cumulativity without forcing strict constraints. | Gaëtan Gilbert | 2018-03-09 |
| | | | | | | | | | | | | | | | | | | | | | | | | Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible. | ||
* | Merge PR #6895: [compat] Remove "Refolding Reduction" option. | 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. | ||
| * | [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. | ||
* | Merge PR #6899: [compat] Remove "Standard Proposition Elimination" | 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 #6462: Sanitize universe declaration in Context (stop using a ref...) | Maxime Dénès | 2018-03-07 |
|\ \ \ \ | |||
| | | * | | 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 |
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | | | |||
| | | * | | | 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. | ||
| | * | | | | [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 |
|\ \ \ | |||
| | * | | 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. | ||
| | | * | [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 |
| |/ | |||
* / | Fix #6878: univ undefined for [with Definition] bad instance size. | Gaëtan Gilbert | 2018-03-01 |
|/ | |||
* | Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism). | Maxime Dénès | 2018-02-24 |
|\ | |||
* \ | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred` | Maxime Dénès | 2018-02-21 |
|\ \ | |||
* \ \ | Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585) | Maxime Dénès | 2018-02-21 |
|\ \ \ | |||
* \ \ \ | Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just ↵ | Maxime Dénès | 2018-02-21 |
|\ \ \ \ | | | | | | | | | | | | | | | | the concl | ||
| | | | * | Fixes bug #6774 (anomaly with ill-typed template polymorphism). | Hugo Herbelin | 2018-02-20 |
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | Computation of the sort of the inductive type was done before ensuring that the arguments of the inductive type had the correct types, possibly brutally failing with `NotArity` in case one of the types expected to be typed with an arity was not so. | ||
| | * | | Adding a test for wish #5532. | Hugo Herbelin | 2018-02-20 |
| |/ / |/| | | |||
| * | | Fix #6529: nf_evar_info and check the env evars' not just the concl | Matthieu Sozeau | 2018-02-19 |
| | | | |||
| | * | Extend `zify_N` with knowledge about `N.pred` | Joachim Breitner | 2018-02-14 |
| |/ |/| | | | | | | | by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602. | ||
* | | Merge PR #6713: Fix #6677: Critical bug with VM and universes | Maxime Dénès | 2018-02-14 |
|\ \ | |/ |/| | |||
| * | Add test case for #6677. | Maxime Dénès | 2018-02-12 |
| | | |||
* | | Merge PR #1047: Support universe instances on the literal Type | Maxime Dénès | 2018-02-12 |
|\ \ | |/ |/| | |||
* | | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | 2018-01-31 |
|\ \ | |||
* | | | Add test case for #5286. | Maxime Dénès | 2018-01-29 |
| | | | |||
| | * | Support universe instances on the literal Type | Tej Chajed | 2018-01-26 |
| |/ |/| | | | | | Fixes BZ#5726. | ||
* | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | Maxime Dénès | 2018-01-22 |
|\ \ | |||
* \ \ | Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints. | Maxime Dénès | 2018-01-22 |
|\ \ \ | |||
| * | | | Add test-suite file for issue #6617. | Cyprien Mangin | 2018-01-19 |
| | | | | |||
* | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | Maxime Dénès | 2018-01-18 |
|\ \ \ \ | |/ / / |/| | | | |||
* | | | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop) | Maxime Dénès | 2018-01-17 |
|\ \ \ \ | |||
| | | * | | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction | Jasper Hugunin | 2018-01-17 |
| |_|/ / |/| | | | |||
| | * | | Use let-in aware prod_applist_assum in dtauto and firstorder. | Jasper Hugunin | 2018-01-17 |
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt). | ||
| | * | Cleanup name-binding structure for fresh evar name generation. | Pierre-Marie Pédrot | 2018-01-02 |
| |/ |/| | | | | | | | | | | | We simply use a record and pack the rel and var substitutions in it. We also properly compose variable substitutions. Fixes #6534: Fresh variable generation in case of clash is buggy. |