aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Expand)Author
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
2017-09-19Fixing bug #5741 (anomaly in info_trivial).Hugo Herbelin
2017-09-19Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Maxime Dénès
2017-09-15Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Maxime Dénès
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Maxime Dénès
2017-09-15Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Maxime Dénès
2017-09-14Avoid extra failure in the "constructor" tactic (bug #5666).Guillaume Melquiond
2017-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
2017-08-31Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projectionsMaxime Dénès
2017-08-31Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateMaxime Dénès
2017-08-31Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagMaxime Dénès
2017-08-30Fixing part of #5707 (allowing destruct to use non dependent case analysis).Hugo Herbelin
2017-08-29Properly handling parameters of primitive projections in cctac.Pierre-Marie Pédrot
2017-08-29Fix BZ#5697: Congruence does not work with primitive projections.Pierre-Marie Pédrot
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...Maxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29Dropping former fix to bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-25primproj: fix bug 5245, hnf on proj with simpl never flag.Matthieu Sozeau
2017-08-24Program: fix BZ#5683, missing lift when building case predicateMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 17:59:33 +0000