aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
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.
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-08More examples about shelve/given_up in tactic-in-terms.Hugo Herbelin
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
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.
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
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.
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
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.
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04ssr: add Prenex Implicits for Some_inj to use it as a viewAnton Trunov
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-03Removing test for bug #2850.Pierre-Marie Pédrot
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.
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
Following up on #6791, we remove the option "Standard Proposition Elimination"
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-02-24Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Maxime Dénès
2018-02-21Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Maxime Dénès
2018-02-21Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Maxime Dénès
2018-02-21Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just ↵Maxime Dénès
the concl
2018-02-20Fixes bug #6774 (anomaly with ill-typed template polymorphism).Hugo Herbelin
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.
2018-02-20Adding a test for wish #5532.Hugo Herbelin
2018-02-19Fix #6529: nf_evar_info and check the env evars' not just the conclMatthieu Sozeau
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602.
2018-02-14Merge PR #6713: Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-12Add test case for #6677.Maxime Dénès
2018-02-12Merge PR #1047: Support universe instances on the literal TypeMaxime Dénès
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-29Add test case for #5286.Maxime Dénès
2018-01-26Support universe instances on the literal TypeTej Chajed
Fixes BZ#5726.
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-22Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Maxime Dénès
2018-01-19Add test-suite file for issue #6617.Cyprien Mangin
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
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).
2018-01-02Cleanup name-binding structure for fresh evar name generation.Pierre-Marie Pédrot
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.
2017-12-18Merge PR #6436: Fix #5368: Canonical structure unification fails.Maxime Dénès
2017-12-15Fix #5368: Canonical structure unification fails.Pierre-Marie Pédrot
Universe instances were lost during constructions of the canonical instance.
2017-12-14Add tactics to reset and display the Ltac profileJason Gross
This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
2017-12-14Merge PR #6386: Catch errors while coercing 'and' intro patternsMaxime Dénès
2017-12-11Allow LtacProf tactics to be calledJason Gross
This fixes #6378. Previously the ML module was never declared anywhere. Thanks to @cmangin for the pointer.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 06:54:32 +0000