aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Collapse)AuthorAge
* Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵Gravatar Gaëtan Gilbert2018-05-14
|\ | | | | | | symlink from repo
| * Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoGravatar Ralf Jung2018-05-13
| | | | | | | | Fixes #7065
* | Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Gravatar Hugo Herbelin2018-05-10
| |
* | Fixes part 1 of #7462 (only-printing not to override existing interp rule).Gravatar Hugo Herbelin2018-05-10
|/
* [ltac] Deprecate nameless fix/cofix.Gravatar Emilio Jesus Gallego Arias2018-04-13
| | | | | | | | | | | | LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
* Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by ↵Gravatar Jason Gross2018-04-12
|\ | | | | | | removing the test.
* | Fix the status of some resolved bugsGravatar Tej Chajed2018-04-11
| |
* | Fix #6956: Uncaught exception in bytecode compilationGravatar Maxime Dénès2018-04-06
| | | | | | | | We also make the code of [compact] in kernel/univ.ml a bit clearer.
| * Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.Gravatar Théo Zimmermann2018-04-05
|/ | | | | Since this is an open bug, it is of lesser importance but non-deterministic tests are a real problem OTOH.
* 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 #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \
* \ \ 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
| | |
| | * Extend `zify_N` with knowledge about `N.pred`Gravatar Joachim Breitner2018-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 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 01:38:13 +0000