aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2017-11-21Merge PR #6178: Have the coq_makefile timing test-suite print moreMaxime Dénès
2017-11-21Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesMaxime Dénès
2017-11-20Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
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-17Have the coq_makefile timing test-suite print moreJason Gross
2017-11-16Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with lo...Maxime Dénès
2017-11-16Merge PR #6104: Fixing encoding in coqdoc output tests.Maxime Dénès
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-15Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Maxime Dénès
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-13Fixing encoding in coqdoc output tests.Hugo Herbelin
2017-11-13Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Maxime Dénès
2017-11-08Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 15:55:59 +0000