aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2015-01-06Fixing test for bug #2830.Pierre-Marie Pédrot
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2015-01-04Adapting two files from test-suite to now forbidden Require's in modules.Hugo Herbelin
2015-01-03Fixing #3896 (incorrect sigma given to printer).Hugo Herbelin
2015-01-03Fixing #3895 (thanks to PMP for diagnosis).Hugo Herbelin
2015-01-01An optimization in the use of unification candidates so as to get theHugo Herbelin
2014-12-30Fixing #3892: Ensure that notation variables do not capture namesHugo Herbelin
2014-12-27include test-suite/coqchk in the summary logEnrico Tassi
2014-12-26new test for coqchkEnrico Tassi
2014-12-19Better doc and a few fixes for Proof using.Enrico Tassi
2014-12-19Fixing wrong notation level in #3295.Hugo Herbelin
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-17Future: blocking by defaultEnrico Tassi
2014-12-16#3828 is solved.Hugo Herbelin
2014-12-16Moving #2447 (congruence) to fixed.Hugo Herbelin
2014-12-16Test for #3654.Hugo Herbelin
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-15Adapted test file for About.Pierre Courtieu
2014-12-15Tests for #3848 and #3854.Hugo Herbelin
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-15Tests for Searchxxx commands added and modified.Pierre Courtieu
2014-12-12Two fixes in unification (bugs #3782 and #3709)Matthieu Sozeau
2014-12-11Test suite: keep message in sync with actual file deletions.Xavier Clerc
2014-12-11New reproduction cases for the test suite.Xavier Clerc
2014-12-10Fixing orientation of postponed subtyping problems.Hugo Herbelin
2014-12-10typoEnrico Tassi
2014-12-10test-suite: few tests for ".v -> .vi -> .vo" compilation chainEnrico Tassi
2014-12-07Improving evar restriction (this is a risky change, as I remember aHugo Herbelin
2014-12-05Commits on evar-evar unification fixed HoTT_coq_106 and improved theHugo Herbelin
2014-12-04Take benefit of improved name preservation of evars in e2fa65fcc.Hugo Herbelin
2014-12-03Updading test-suite.Hugo Herbelin
2014-12-02When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifHugo Herbelin
2014-12-01Fixing test-suite.Pierre-Marie Pédrot
2014-11-30Adding test for bug #3417.Pierre-Marie Pédrot
2014-11-30Test for bug #3485.Pierre-Marie Pédrot
2014-11-30Test for bug #3487.Pierre-Marie Pédrot
2014-11-30Test of bug #3682.Pierre-Marie Pédrot
2014-11-27Fix test flags for fake_ideEnrico Tassi
2014-11-25Bug #3804 is actually closed (thanks to Jason Gross for the notification).Xavier Clerc
2014-11-25Tweak some test cases.Xavier Clerc
2014-11-25Adapting to current semantics of "simpl non-evaluable-cst"Hugo Herbelin
2014-11-25Experimenting using unification when matching evar/meta free subtermsHugo Herbelin
2014-11-24Adding test for bug #3248.Pierre-Marie Pédrot
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-11-22Test for closed #2713 and #2876.Hugo Herbelin
2014-11-22Add test-suite file for dependent rewriting example by Vadim Zaliva andMatthieu Sozeau
2014-11-21Adding test for bug #3326.Pierre-Marie Pédrot
2014-11-21Adding test for bug #3424.Pierre-Marie Pédrot
2014-11-21Cleaning up closed bugs in test-suite.Pierre-Marie Pédrot
2014-11-21Test for bug #3788.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 14:15:54 +0000