aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2015-06-24Extend test-suite for the positivity checker.Arnaud Spiwack
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-23Fixing incompatibility introduced with simpl in commit 364decf59c1 (orHugo Herbelin
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-11Add test-suite file for bug #3446.Matthieu Sozeau
2015-06-09STM: states coming from workers have no proof terminators (Close #4246)Enrico Tassi
2015-06-09STM: silly mistake in jumping back to an old state (Close #4249)Enrico Tassi
2015-06-02Adding a test for bug #4057.Pierre-Marie Pédrot
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-29Flag -test-mode intended to be used for ad-hoc prints in test-suiteEnrico Tassi
2015-05-28STM: preserve branch name on edit (Close: #4245, #4246)Enrico Tassi
2015-05-28Test for 4159Enrico Tassi
2015-05-19Test for bug #4116.Pierre-Marie Pédrot
2015-05-18Removing test for opened bugs that were already present in the closed test-su...Pierre-Marie Pédrot
2015-05-18Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Pierre-Marie Pédrot
2015-05-18Removing option -no-native-compiler from test #3539 since this option is nowHugo Herbelin
2015-05-15Removing option -no-native-compiler from test #3539 since this option is nowHugo Herbelin
2015-05-15Turning "Set Regular Subst Tactic" on by default (for 8.6).Hugo Herbelin
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-14#3953 now closed.Hugo Herbelin
2015-05-13Fixing bug #4216:Pierre-Marie Pédrot
2015-05-13Better fixing #4198 such that the term to match is looked for beforeHugo Herbelin
2015-05-12Extraction: fix the detection of the "polyprop" situationPierre Letouzey
2015-05-12Test for bug #4234.Pierre-Marie Pédrot
2015-05-11Test for bug #4232.Pierre-Marie Pédrot
2015-05-09Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Hugo Herbelin
2015-05-09Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forHugo Herbelin
2015-05-06Fixing treatment of recursive equations damaged by 857e82b2ca0d1.Hugo Herbelin
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-01Fixing computation of implicit arguments by position in fixpoints (#4217).Hugo Herbelin
2015-05-01Giving to "subst" a more natural semantic (fixing #4214) by using allHugo Herbelin
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-22Test for #4198 (appcontext in return clause of match).Hugo Herbelin
2015-04-21Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentHugo Herbelin
2015-04-17Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalHugo Herbelin
2015-04-16Test for bug #4190.Pierre-Marie Pédrot
2015-04-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-10Test for bug #3199.Pierre-Marie Pédrot
2015-04-09Better test-suite files, removing reliance on admit.Matthieu Sozeau
2015-04-09Fix declarations of instances to perform restriction of universeMatthieu Sozeau
2015-04-09Add test-suite file for bug #4120.Matthieu Sozeau
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-06Test for bug #3815.Pierre-Marie Pédrot
2015-04-01Fixing test-suite.Pierre-Marie Pédrot
2015-03-31Fixing test-suite.Pierre-Marie Pédrot
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-30camlp4: grep away warnings in output/* testsEnrico Tassi
2015-03-29Adding test for bug #4165.Pierre-Marie Pédrot
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
2015-03-25Another example about the consequence of a wrong computation of theHugo Herbelin