aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
Commit message (Collapse)AuthorAge
* Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Gravatar Hugo Herbelin2018-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)Gravatar Pierre-Marie Pédrot2018-04-01
|\
* | Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
| |
* | Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Gravatar Pierre-Marie Pédrot2018-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).Gravatar Hugo Herbelin2018-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.Gravatar Gaëtan Gilbert2018-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.Gravatar Maxime Dénès2018-03-09
|\
* | More examples about shelve/given_up in tactic-in-terms.Gravatar Hugo Herbelin2018-03-08
| |
* | Proof engine: support for nesting tactic-in-term within other tactics.Gravatar Hugo Herbelin2018-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.Gravatar Emilio Jesus Gallego Arias2018-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"Gravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Gravatar Maxime Dénès2018-03-07
|\ \ \
* \ \ \ Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Gravatar Maxime Dénès2018-03-07
|\ \ \ \
| | | * | ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Enrico Tassi2018-03-06
| | | | |
* | | | | Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | | * | | Sanitize universe declaration in Context (stop using a ref...)Gravatar Gaëtan Gilbert2018-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.Gravatar Emilio Jesus Gallego Arias2018-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.Gravatar Théo Zimmermann2018-03-04
| |/ / /
| | * / ssr: add Prenex Implicits for Some_inj to use it as a viewGravatar Anton Trunov2018-03-04
| |/ /
* | | Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ | |/ / |/| |
* | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \
| | * | Removing test for bug #2850.Gravatar Pierre-Marie Pédrot2018-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"Gravatar Emilio Jesus Gallego Arias2018-03-03
| | |/ | | | | | | | | | Following up on #6791, we remove the option "Standard Proposition Elimination"
| * | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | |
| * | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| |/
* / Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
|/
* Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\
* \ Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Gravatar Maxime Dénès2018-02-21
|\ \
* \ \ Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just ↵Gravatar Maxime Dénès2018-02-21
|\ \ \ | | | | | | | | | | | | the concl
| | | * Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Hugo Herbelin2018-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.Gravatar Hugo Herbelin2018-02-20
| |/ |/|
| * Fix #6529: nf_evar_info and check the env evars' not just the conclGravatar Matthieu Sozeau2018-02-19
| |
* | Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\ \ | |/ |/|
| * Add test case for #6677.Gravatar Maxime Dénès2018-02-12
| |
* | Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\ \ | |/ |/|
* | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \
* | | Add test case for #5286.Gravatar Maxime Dénès2018-01-29
| | |
| | * Support universe instances on the literal TypeGravatar Tej Chajed2018-01-26
| |/ |/| | | | | Fixes BZ#5726.
* | Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Gravatar Maxime Dénès2018-01-22
|\ \
| * | Add test-suite file for issue #6617.Gravatar Cyprien Mangin2018-01-19
| | |
* | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \ \ | |/ / |/| |
* | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Maxime Dénès2018-01-17
|\ \ \
| | * | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-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.Gravatar Pierre-Marie Pédrot2018-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.
* | Merge PR #6436: Fix #5368: Canonical structure unification fails.Gravatar Maxime Dénès2017-12-18
|\ \
| * | Fix #5368: Canonical structure unification fails.Gravatar Pierre-Marie Pédrot2017-12-15
| | | | | | | | | | | | Universe instances were lost during constructions of the canonical instance.
* | | Add tactics to reset and display the Ltac profileGravatar Jason Gross2017-12-14
|/ / | | | | | | | | This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
* | Merge PR #6386: Catch errors while coercing 'and' intro patternsGravatar Maxime Dénès2017-12-14
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-31 05:40:16 +0000