aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2019-02-18Merge PR #9509: Fix #9508: Unexpected interaction between implicit arguments ...Maxime Dénès
2019-02-17Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.Pierre-Marie Pédrot
2019-02-14Merge PR #9502: Remove nondeterministic testsThéo Zimmermann
2019-02-13more testsEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
2019-02-11Fix #9508: Unexpected interaction between implicit arguments and primitive pr...Pierre-Marie Pédrot
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
2019-02-07Remove nondeterministic testsGaëtan Gilbert
2019-02-06Avoid eqn when generating name in induction_gen.Jasper Hugunin
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Enrich implicits for instancesJasper Hugunin
2019-02-04Merge PR #9317: Restrict universes in records.Pierre-Marie Pédrot
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
2019-02-04Merge PR #9454: Fix off-by-one error in nat syntax warningsPierre-Marie Pédrot
2019-02-04Merge PR #9452: [proof] optimize proof always works on incomplete proofsPierre-Marie Pédrot
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
2019-01-31add testEnrico Tassi
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-30Restrict universes in records.Gaëtan Gilbert
2019-01-29Update update-compat.py scriptJason Gross
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-24Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)Matthieu Sozeau
2019-01-23Merge PR #9270: Turn `Refine instance Mode` off by defaultPierre-Marie Pédrot
2019-01-22Fixing #9329 (registering empty levels in the order they are recomputed).Hugo Herbelin
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Make `Add Morphism` not rely on Refine InstanceMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-22[CS] recognize applied primitive projections as keys (fix #9375)Enrico Tassi
2019-01-20Discard argument names of section variables on section closeJasper Hugunin
2019-01-14Merge PR #9307: Handle local definitions in implicit arguments of InstanceMaxime Dénès
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2019-01-09Make some tests more robust by adding missing proof terminatorsMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` p...Maxime Dénès
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
2018-12-30Do not take universes into account in lia reification.Pierre-Marie Pédrot
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost o...Gaëtan Gilbert
2018-12-12Fixes #9166 (no warning on pattern variables named like a deprecated alias).Hugo Herbelin
2018-12-11Tests for #4509, #6202 which happen to be fixed (was a lost of evars in shelf).Hugo Herbelin
2018-12-05Add test for #8951.Gaëtan Gilbert
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 15:33:32 +0000