aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-04-14Merge PR #11978: Close #11935: section variables do not have universe instances.Pierre-Marie Pédrot
2020-04-14Merge PR #11985: Fix #11934 equality on constrexpr ignores instances of expli...Pierre-Marie Pédrot
2020-04-13Close #11935: section variables do not have universe instances.Gaëtan Gilbert
2020-04-13Fix #11783 Require in SectionGaëtan Gilbert
2020-04-13Partial import inductive(..)Gaëtan Gilbert
2020-04-13test partial importGaëtan Gilbert
2020-04-13Add specific test for "useless" syndefGaëtan Gilbert
2020-04-13Simplifying the declaration of constants bound to primitive projections.Hugo Herbelin
2020-04-12Exporting BEST as OPT for the tests using coq_makefile-generated Makefile.Hugo Herbelin
2020-04-12[test-suite] Remove deprecated -I option of coqchk in MakefilePierre Roux
2020-04-11Fix #7812Attila Gáspár
2020-04-11If a custom entry has global, a bound variable is valid in this entry.Hugo Herbelin
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ...Hugo Herbelin
2020-04-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
2020-04-06Fix #11934 equality on constrexpr ignores instances of explicit applicationsGaëtan Gilbert
2020-04-06Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_stateMatthieu Sozeau
2020-04-05Fixes #11194 (Canonical/Coercion not located for coqdoc).Hugo Herbelin
2020-04-03Improve error messages for Set and Unset commands.Théo Zimmermann
2020-04-03Fix the test for bug #4544.Pierre-Marie Pédrot
2020-04-01add tests for notations with sigma typesOlivier Laurent
2020-04-01Merge PR #11945: Fix #11941: anomaly in equality schemesEmilio Jesus Gallego Arias
2020-03-31Merge PR #11933: Fix calling test suite makefile with a dune built coqEmilio Jesus Gallego Arias
2020-03-31Include review suggestionsGaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-31Merge PR #11684: Remove spurious anomalies in kernel reductionPierre-Marie Pédrot
2020-03-31Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the gr...Maxime Dénès
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Fix #11941: anomaly in equality schemesGaëtan Gilbert
2020-03-27Helping issue #11659 by leaving only the Cast hack in the grammar.Hugo Herbelin
2020-03-27Merge PR #11848: Nicer printing for decimal constantsHugo Herbelin
2020-03-26Fix calling test suite makefile with a dune built coqGaëtan Gilbert
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-26Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlibHugo Herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
2020-03-25Nicer printing for decimal constants in QPierre Roux
2020-03-25Nicer printing for decimal constants in RPierre Roux
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
2020-03-22Testing notations which are specific numerals.Hugo Herbelin
2020-03-22Adding a test for printing single characters.Hugo Herbelin
2020-03-22Test-suite: Assume coqtop output is text even with non-printable characters.Hugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
2020-03-19Remove spurious anomalies in kernel reductionGaëtan Gilbert
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 13:47:32 +0000