aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Collapse)Author
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
This has been in the TODO queue for a long time, and indeed I have recently seen some trouble with users passing two .v files to Coq, which it isn't a) tested, b) supported. Moreover, it doesn't even work correctly in 8.13 due to some other changes in the toplevel related to auxiliary files. (*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-01-26[vernac] Check that no proofs do remain open at section/module closing timeEmilio Jesus Gallego Arias
Fixes #13755 .
2021-01-18Fixes #13413: freshness issue with "%" introduction pattern.Hugo Herbelin
We build earlier the final expected name at the end of a sequence of "%" introduction patterns.
2021-01-11Fix #13732: Implicit Type vs universesGaëtan Gilbert
This returns to the previous behaviour of Implicit Type forgetting universes. `Implicit Type T : Type@{u}.` may be confusing as it is equivalent to `: Type`, but until we have a better idea of what to do with anonymous types I see no other solution, especially in the short term to fix the bug.
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04EConstr iterators respect the binding structure of cases.Pierre-Marie Pédrot
Fixes #3166.
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 04:58:38 +0000