aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-04-23[ssr] under: Strenghten over & Add test_big_andbErik Martin-Dorel
2019-04-23[ssr] under: Extend the test-suite to exemplify most use casesErik Martin-Dorel
2019-04-23[ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over"Erik Martin-Dorel
2019-04-23[ssr] under: Rename bound variables a posteriori for cosmetic purposeEnrico Tassi
2019-04-20Merge PR #9906: coq_makefile install target: error if any file is missingEnrico Tassi
2019-04-16Fix spurious argument of {measure}Maxime Dénès
2019-04-16Take advantage of relaxed {measure} syntax in test suiteMaxime Dénès
2019-04-08coq_makefile install target: error if any file is missingGaëtan Gilbert
2019-04-08Merge PR #9900: [native compiler] Fix critical bug with stuck primitive proje...Pierre-Marie Pédrot
2019-04-06Fix numeral notations test in async mode.Gaëtan Gilbert
2019-04-06Fix pretty-printing of primitive integersErik Martin-Dorel
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
2019-04-03Merge PR #8638: Remove -compat 8.7Théo Zimmermann
2019-04-02[ssr] implement "under i: ext_lemma" by rewrite ruleEnrico Tassi
2019-04-02[ssr] under: rewrite takes an optional bool argErik Martin-Dorel
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-04-02Remove -compat 8.7Jason Gross
2019-04-02Merge PR #9659: Fix #9652: rewrite fails to detect lack of progressEmilio Jesus Gallego Arias
2019-04-02Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)Pierre Roux
2019-04-02Make R parser parse decimals (e.g., 1.02e+01)Pierre Roux
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
2019-04-01Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and ...Vincent Laporte
2019-04-01Add test-case for #9840Jason Gross
2019-04-01Several improvements and fixes of LiaFrédéric Besson
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-04 11:07:08 +0000