aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc
AgeCommit message (Expand)Author
2020-11-12Add the test as a misc script.Pierre-Marie Pédrot
2020-10-27Rename operconstr -> termJim Fehrle
2020-09-18[lib] make canonical_path_name always absolute (fix #13031)Enrico Tassi
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
2020-03-06Adding a test to the test-suite.Pierre-Marie Pédrot
2019-12-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...charguer
2019-11-01Implementing support for vos/vok files.charguer
2019-10-18Adding a test for votour.Pierre-Marie Pédrot
2019-07-21Dune: fix build_all_stdlib ruleGaëtan Gilbert
2019-07-02[test-suite] Fix evil plugin after changes in declare API.Emilio Jesus Gallego Arias
2019-06-26Merge PR #10401: Fix printers testEmilio Jesus Gallego Arias
2019-06-24[test-suite] Fix printers testGaëtan Gilbert
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-18[lexer] correctly update line number when lexing QUOTATION (fix #10350)Enrico Tassi
2019-05-28Fix printers.sh test when missing coqtop.byte, print more infoGaëtan Gilbert
2019-05-22Fix changelog test file on macOS: do not use ls + wc.Théo Zimmermann
2019-05-22Use grep in changelog test instead of adhoc readsGaëtan Gilbert
2019-05-08Add a test that unreleased changelog of released versions is empty.Théo Zimmermann
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-06Makefiles: Fixes for byte compilationGaëtan Gilbert
2019-02-04[dune] Fix Dune build in Windows.Emilio Jesus Gallego Arias
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2018-11-16Add test for Include in -quick modeGaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-02gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlGaëtan Gilbert
2018-10-19Porting the test-suite to coqpp.Pierre-Marie Pédrot
2018-10-11[dune] [test-suite] Support for running the test suite with Dune.Emilio Jesus Gallego Arias
2018-09-13Add test for inconsistency from polymorphism capturing global univsGaëtan Gilbert
2018-06-22Fix #7704: get_toplevel_path needs normalised argv.(0)Gaëtan Gilbert
2018-06-07add test for #7595Ralf Jung
2018-05-16Merge PR #7484: Fix non-portable shebang in test-suite.Enrico Tassi
2018-05-14Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling s...Gaëtan Gilbert
2018-05-13Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoRalf Jung
2018-05-11Fix non-portable shebang in test-suite.Théo Zimmermann
2018-05-09test for coqc -oEnrico Tassi
2018-04-05Improve shell scriptszapashcanon
2017-09-13Adding a test for utf8 characters in directory names.Hugo Herbelin
2017-07-20Remove trailing CR before diff in output and misc tests.Maxime Dénès
2017-06-21Should fix a false negative reported by deps-order.sh.Hugo Herbelin
2017-06-11A stronger test that #use"include";; works well.Hugo Herbelin
2017-05-10Moving code for miscellaneous tests to specific files.Hugo Herbelin
2017-05-10Adding tests for testing exit status and #use"include".Hugo Herbelin
2017-05-10Cleaning old untested not any more interesting testing files.Hugo Herbelin
2016-07-04test-suite: test checking of libraries checksum.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:55:40 +0000