aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2017-11-08Remove dependency of test-suite on git (fix #5725).Théo Zimmermann
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime 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 #5989: Handle ∞ in coq-makefile timing test-suiteMaxime Dénès
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
2017-10-19Handle ∞ in coq-makefile timing test-suiteJason Gross
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
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-10Use a nice printer for constant names in Suggest Proof Using.Gaëtan Gilbert
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert
2017-10-10Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Maxime Dénès
2017-10-09Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism`...Maxime Dénès
2017-10-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...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-05[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Emilio Jesus Gallego Arias
2017-10-05romega: takes advantage of context variables with bodyPierre Letouzey
2017-10-05Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...Pierre Letouzey
2017-10-05Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Maxime Dénès
2017-10-05Merge PR #1107: Add coqwc tests to test suiteMaxime Dénès
2017-10-05Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5...Maxime Dénès
2017-10-05Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...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 #1078: Report missing arguments in error messageMaxime Dénès
2017-10-04Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Maxime Dénès
2017-10-03add coqwc testsPaul Steckler
2017-10-03Merge PR #1012: Make a test for coq_makefile portable.Maxime Dénès
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-27Moving setting of "cleared" evar flag directly in Evd.restrict.Hugo Herbelin
2017-09-27Fixing an old bug in collecting evars with cleared context.Hugo Herbelin
2017-09-27Fixing an old bug in collecting evars with cleared context.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-06 23:26:58 +0000