aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2017-11-23Recognizing Z in romega up to conversion.Hugo Herbelin
2017-11-23Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Hugo Herbelin
2017-11-23Fixing a 8.7 regression of ring_simplify in ArithRing.Hugo Herbelin
2017-11-23Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Maxime Dénès
2017-11-22Fix universe polymorphic Program obligations.Matthieu Sozeau
2017-11-20Merge PR #6166: Fix regression in treating Defined as definedMaxime Dénès
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Maxime Dénès
2017-11-20Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbo...Maxime Dénès
2017-11-19Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gaëtan Gilbert
2017-11-15Fix regression in treating Defined as definedTej Chajed
2017-11-15Fix #5761: cbv on undefined evars under binders produces unbound relGaëtan Gilbert
2017-11-14Fixes #6129 (declaration of coercions made compatible with local definitions).Hugo Herbelin
2017-11-14One more step in fixing #5762 ("where" clause).Hugo Herbelin
2017-11-13Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Maxime Dénès
2017-11-06Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to al...Maxime Dénès
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
2017-11-05Refining PR#924 (insensitivity of projection heuristics to alphabet).Hugo Herbelin
2017-11-04Adding support for syntax "let _ := e in e'" in Ltac.Hugo Herbelin
2017-11-03Merge PR #6047: A generic printer for ltac valuesMaxime Dénès
2017-11-03Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous varia...Maxime Dénès
2017-11-03Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Maxime Dénès
2017-11-02Binding ltac printing functions to the system of generic printing.Hugo Herbelin
2017-10-30Fixing #2881 ("change with" failing in an Ltac definition).Hugo Herbelin
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
2017-10-27Merge PR #677: Trunk+abstracting injection flagsMaxime Dénès
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
2017-10-25Put newlines at the end of files.Gaëtan Gilbert
2017-10-23Move bug files to match their new GitHub ID (fixes #6001).Théo Zimmermann
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
2017-10-17Adding a test for bug BZ#5692.Pierre-Marie Pédrot
2017-10-15[stdlib] Fix warnings on deprecated `Add Setoid`Emilio Jesus Gallego Arias
2017-10-10Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Maxime Dénès
2017-10-06Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...Maxime Dénès
2017-10-06Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...Maxime Dénès
2017-10-06Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly BZ#4...Maxime Dénès
2017-10-05Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...Pierre Letouzey
2017-10-05Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5...Maxime Dénès
2017-10-05Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...Pierre Letouzey
2017-10-05Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Hugo Herbelin
2017-10-05Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Hugo Herbelin
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-10-04Merge PR #1006: fix: ssrmatching and primitive projectionsMaxime Dénès
2017-10-04Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Maxime Dénès
2017-09-27Moving setting of "cleared" evar flag directly in Evd.restrict.Hugo Herbelin
2017-09-25Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...Maxime Dénès
2017-09-25Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...Maxime Dénès
2017-09-23Fixing #5755 (discharging of inductive types not correct with let-ins).Hugo Herbelin
2017-09-23Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Hugo Herbelin
2017-09-21A possible fix to BZ#5750 (ability to print context of ltac subterm match).Hugo Herbelin
2017-09-20ssr: fix canonical strucut key comparison with primproj onEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 21:59:38 +0000