aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-04-01Merge PR #9872: Fix timing diff script to support non-utf8Emilio Jesus Gallego Arias
2019-03-31[pretty-timing scripts] Don't barf on non-utf-8Jason Gross
2019-03-31Remove test file with Timeout that failed spuriously.Théo Zimmermann
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
2019-03-27Merge PR #9837: Fix some critical-bugs informationsThéo Zimmermann
2019-03-26Fix reproduction info for some past critical bugsGaëtan Gilbert
2019-03-26Merge PR #9690: Fix 9663 (Miller pattern unification fails on evars)Matthieu Sozeau
2019-03-26Merge PR #9489: [ssr] avoid HO unification to perform truncation analysy in elimMaxime Dénès
2019-03-26[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)Enrico Tassi
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-03-25[ssr] avoid HO unif when doing truncation analysisEnrico Tassi
2019-03-25Fix #9652: rewrite fails to detect lack of progressGaëtan Gilbert
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...Maxime Dénès
2019-03-20Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on applic...Gaëtan Gilbert
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
2019-03-14Relax the ambiguous path condition of coercionKazuhiko Sakaguchi
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Test for SkySkimmer/coq#13Gaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Fix Require in output test for reals syntaxGaëtan Gilbert
2019-03-13Merge PR #9736: Don't coqchk the test suite prerequisitesEnrico Tassi
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ...Emilio Jesus Gallego Arias
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-03-11Don't coqchk the test suite prerequisitesGaëtan Gilbert
2019-03-05Remove regularly failing test from test-suite.Théo Zimmermann
2019-03-04Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)Emilio Jesus Gallego Arias
2019-03-04[stm] unfocus when edition exits the proof (fix #9431)Enrico Tassi
2019-03-01Set COQLIB so the test suite will run locally on Windows.Jim Fehrle
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-25add testcase for primitive projectionEnrico Tassi
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-25add testcase for fixEnrico Tassi
2019-02-25add test case for "match"Enrico Tassi
2019-02-22Merge PR #9364: Apply implicit binders to Hypothesis inside sections.Gaëtan Gilbert
2019-02-22Merge PR #9576: [library] Remove `-boot` option.Enrico Tassi
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-20[azure] [ci] Build on Windows using Dune.Emilio Jesus Gallego Arias
2019-02-19Merge PR #9297: Two fixes in printing notations with patternsEmilio Jesus Gallego Arias
2019-02-19Notations: Fixing a printing bug with patterns.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 04:47:04 +0000