aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for ↵coqbot-app[bot]
cumulative inductive types Reviewed-by: SkySkimmer
2020-11-28Merge PR #13502: A small fix for freshness in the `change` tacticcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ↵Matthieu Sozeau
types
2020-11-27A small fix for freshness in the `change` tacticJasper Hugunin
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to ↵Pierre-Marie Pédrot
check resolution of evars more incrementally Ack-by: SkySkimmer Reviewed-by: gares Ack-by: ppedrot
2020-11-26Fixes #13456: regression where tactic exists started to check evars ↵Hugo Herbelin
incrementally. The regression was due to #12365. We fix it by postponing the evars check after the calls to the underlying constructor tactic, while retaining using information from the first instantiations to resolve the latter instantiations.
2020-11-25Add tests for #13303Gaëtan Gilbert
2020-11-24Merge PR #13455: Fix comparison of extracted array literalscoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-24Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction ↵coqbot-app[bot]
of universes in "Context" Reviewed-by: SkySkimmer
2020-11-23Fix comparison of extracted array literalsGaëtan Gilbert
Fixes #13453 which was a loop in ~~~ocaml let normalize a = let o = optims () in let rec norm a = let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in if eq_ml_ast a a' then a else norm a' in norm a ~~~ the `eq_ml_ast` was always returning `false`.
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-22Fixes another instance of bug #7967: restriction of universes in "Context".Hugo Herbelin
2020-11-20Merge PR #13305: Only lower inductives to Prop if the type is syntactically ↵Pierre-Marie Pédrot
an arity. Reviewed-by: ppedrot
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized ↵coqbot-app[bot]
binder Reviewed-by: herbelin
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a ↵coqbot-app[bot]
primitive projection was wrongly supposed to be already inferred Reviewed-by: gares
2020-11-20Merge PR #13371: Extend hack to use postponed constraints in retyping to ↵coqbot-app[bot]
template poly Reviewed-by: gares Reviewed-by: herbelin
2020-11-19Fixes #9971: expand_projections failing on primitive projections of unknown ↵Hugo Herbelin
type. This was a case where expand_projections was calling find_mrectype which was expecting the argument of the projection to be an inductive. We could have ensured that this type is at least the appropriate inductive applied to fresh evars, but this expand_projections was in practice used for checking the applicability of canonical structures and the unifiability of the parameters of the projections is anyway a consequence of the unifiability of the principal argument of the projections. So, the latter is enough.
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas ↵Pierre-Marie Pédrot
(hopefully) Reviewed-by: ppedrot
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
Reviewed-by: gares
2020-11-16Fix incorrect name refreshing when interning a generalized binderGaëtan Gilbert
Fix #13249
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context ↵coqbot-app[bot]
of the definition of the metas Reviewed-by: mattam82
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part ↵coqbot-app[bot]
of unification Reviewed-by: mattam82
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
It remains to accept resolving Type(u)<=Prop for u arbitrary sort variable.
2020-11-16Extend hack to use postponed constraints in retyping to template polyGaëtan Gilbert
See 742ef62fe8050a6865d06bd644e30cbec0e7eb02 Fix #13366 Fix #9809
2020-11-16Finish fixing setoid rewrite under anonymous lambdas (hopefully)Gaëtan Gilbert
Fix #13246 Not sure if this is the right thing to do, but it seems to work.
2020-11-16Only lower inductives to Prop if the type is syntactically an arity.Gaëtan Gilbert
Fix #13300
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ↵coqbot-app[bot]
sort elimination constraints Reviewed-by: gares
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation ↵Hugo Herbelin
(solve_simple_eqn). The bug was that an assumption could be interpreted as a local definition and wrongly expanded. It triggered rarely because it involved mixing let-ins and local assumptions + imitation under binders.
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
Fix #6042 Also introduce a deprecated compat option
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-13Fixes #13363: case of a meta not paying attention to being under binders.Hugo Herbelin
In Evar := C[Meta] problems of unification.ml, and C[ ] contains binders, Meta was wrongly considered by pose_all_metas_as_evars as under these binders (while Metas are always defined in the initial context of the unification problem).
2020-11-13Fix incorrect "avoid" set in globenv extra dataGaëtan Gilbert
Fix #13348
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
Fix #13354 This change is very specific to array, but should not be a significant obstacle to generalization of the feature to eg axioms if we want to later.
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
Polymorphic side-effects generated in monomorphic mode would be counted towards trusted subcomponents. This would allow to make ill-typed terms pass as legitimate by mimicking the shape of the inlining of monomorphic side-effects in such a proof.
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause ↵Pierre-Marie Pédrot
of a match. Reviewed-by: ppedrot
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-05Fixes #13216 (use of type classes in the return clause of a match).Hugo Herbelin
This was deactivated in fb1c2a017e but it seems useful (e.g. in contribs containers). It seems to be useful
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-03Merge PR #13132: Understand Mangle Names in implicit generalizationcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13179: Fix printing for empty primitive arrayscoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bugcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding ↵coqbot-app[bot]
notations in patterns Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: LasseBlaauwbroek
2020-11-02Fix printing for empty primitive arraysGaëtan Gilbert
Fix #13178
2020-10-31Closes #13278: take into account elimination constraints in small inversion.Hugo Herbelin
Ideally, if equations t <= ?x were preserving subtyping that could be simpler. Currently we need however to put a rigid universe as constraint on the return predicate so that one branch does not force the return sort to be lower by unification than what another branch would have needed.
2020-10-31Fine-tuning the sort of the predicate obtained by small inversion.Hugo Herbelin
If the result is in SProp, Prop or (impredicative) Set, we preserve this information since the elimination sort might be restricted by the sort of the destructed type. If the result is in Type, we use a fresh sort upper bound so that we are sure not having residual algebraic universes which would raise problems in a type constraint (e.g. in define_evar_as_product). This fixes the part of #13278 posted on discourse.
2020-10-29Fixing interpretation of rewrite_strat argument in Ltac.Hugo Herbelin
Ltac variables were not yet supported.
2020-10-26Adding a test for the second bug.Pierre-Marie Pédrot
2020-10-22Remove test-suite/bugs/opened/bug_3395.v: not a bugGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 03:37:27 +0000