aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-09Merge PR #8726: More robust treatment of the Discharge statusPierre-Marie Pédrot
2019-06-08[Test-suite] Add non-regression test case for #8725Vincent Laporte
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...Pierre-Marie Pédrot
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06Merge PR #10305: Fix SSR (un)fold of polymorphic terms - issue 9336Enrico Tassi
2019-06-06Merge PR #10302: Fix SSR 'case B:b' with universe polymorphic equalityEnrico Tassi
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-05Merge PR #10215: Refine typing of vernacular commandsMaxime Dénès
2019-06-04Fix SSR (un)fold of polymorphic terms - issue 9336Andreas Lynge
2019-06-04Merge PR #10265: Fix #10264: Singleton class field data is erroneous.Matthieu Sozeau
2019-06-04Fix SSR 'case B:b' with universe polymorphic equalityAndreas Lynge
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-05-31Fix #10268: vio2vo produces incorrect term when discharging.Pierre-Marie Pédrot
2019-05-29Merge PR #10270: Fix debug printersEnrico Tassi
2019-05-28Fix printers.sh test when missing coqtop.byte, print more infoGaëtan Gilbert
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-28Fix #10264: Singleton class field data is erroneous.Pierre-Marie Pédrot
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Merge PR #10163: Fix dependencies of new test file and fix macOS issues.Vincent Laporte
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-22Fix dependencies of new test file.Théo Zimmermann
2019-05-22Fix changelog test file on macOS: do not use ls + wc.Théo Zimmermann
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...Hugo Herbelin
2019-05-22Merge PR #10211: Use grep in changelog test instead of adhoc readsThéo Zimmermann
2019-05-22Use grep in changelog test instead of adhoc readsGaëtan Gilbert
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
2019-05-20Merge PR #9530: Remove `VtUnkown` classificationGaëtan Gilbert
2019-05-20Merge PR #9873: Remove test file with Timeout that failed spuriously.Gaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-19Implicit Quantifiers recurse in continuation of let-inJasper Hugunin
2019-05-16Fix #10176: shadowing vs automatic class based generalizationGaëtan Gilbert
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10[Attributes] Allow explicit value for two-valued attributesVincent Laporte
2019-05-10Merge PR #10058: Remove various circumvolutions from reduction behaviorsEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:55:01 +0000