aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-09-03Merge PR #8124: Fix #8121: anomalies in native_compute with let and evars.Maxime Dénès
2018-09-03Merge PR #8359: [ssr] move ssr_*v tests to test-suite/ssr/Maxime Dénès
2018-09-03Merge PR #8107: Fixes #8106: anomaly if declaring levels for only printing th...Emilio Jesus Gallego Arias
2018-09-03Merge PR #8286: Fixing #7867: class error message tried to print a "fun" with...Emilio Jesus Gallego Arias
2018-09-02Fixing #7867 (class error message tries to print a "fun" with no binder).Hugo Herbelin
2018-09-02Fixing #8106 (anomaly if declaring levels for only printing then only parsing).Hugo Herbelin
2018-08-30[ssr] move ssr_*v tests to test-suite/ssr/Enrico Tassi
2018-08-29Merge PR #8167: Fix ordering of before/after in print-pretty-timed-*Enrico Tassi
2018-08-27Update test-suite for focusing on named goals.Théo Zimmermann
2018-08-24Fix ordering of before/after in print-pretty-timed-*Jason Gross
2018-08-06Add regression test for issue #4202Tej Chajed
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-29A test on the different ways to indicate the levels of a rule.Hugo Herbelin
2018-07-27[ci] Remove CircleCI setup.Emilio Jesus Gallego Arias
2018-07-26Add information to option type errorsTej Chajed
2018-07-26Fix #8121: anomalies in native_compute with let and evars.Pierre-Marie Pédrot
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...Pierre-Marie Pédrot
2018-07-26Merge PR #7274: Avoiding introducing dependency on the indices of a term whic...Pierre-Marie Pédrot
2018-07-25Merge PR #8133: Fixes #8126: issue with notations and nested applicationsEmilio Jesus Gallego Arias
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2018-07-25Optimized dependencies for pattern-matching on only trivial patterns.Hugo Herbelin
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
2018-07-24Add simple test cases for vm and native on primitive projections.Gaëtan Gilbert
2018-07-24Fix #7329: coqchk Include with primitive projectionsGaëtan Gilbert
2018-07-24Fixes #8126 (issue with notations and nested applications).Hugo Herbelin
2018-07-24Merge PR #6801: Highlight differences between successive proof steps (color, ...Emilio Jesus Gallego Arias
2018-07-24Merge PR #8083: Add test for repeated section with same nameThéo Zimmermann
2018-07-24Merge PR #8000: Fix #7854: Native compilation + flambda trigger SEGFAULT.Maxime Dénès
2018-07-23Make tokenize_string an optional parameter for diff methods in pp_diffs.Jim Fehrle
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-07-23Add test for repeated section with same nameJasper Hugunin
2018-07-23Make the out_channel for the log file accessible so tests can write to it (e....Jim Fehrle
2018-07-19Merge PR #7941: Extend QuestionMark to produce a better error message in case...Pierre-Marie Pédrot
2018-07-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-07-12[dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias
2018-07-12Fix #7854: Native compilation + flambda trigger SEGFAULT.Pierre-Marie Pédrot
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-09Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Matthieu Sozeau
2018-07-06Add test for #8004.Gaëtan Gilbert
2018-07-04Convert timing tools to run with both python2 and python3Jasper Hugunin
2018-07-03[test suite] Test case for attributesVincent Laporte
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-01Add test for Uniform Inductive ParametersJasper Hugunin
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 03:19:25 +0000