aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
* Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
* test-suite: Fix test-suite MakefileGravatar Matthieu Sozeau2015-07-07
* Test case for #4203, fixed by commit a51cce36.Gravatar Maxime Dénès2015-07-06
* Notation: use same level for "@" in constr: and pattern: (Close: #4272)Gravatar Enrico Tassi2015-07-01
* Fix incompleteness of conversion used by evarconvGravatar Matthieu Sozeau2015-06-28
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.Gravatar Maxime Dénès2015-06-24
* Fixing incompatibility introduced with simpl in commit 364decf59c1 (orGravatar Hugo Herbelin2015-06-23
* Add test-suite file for bug #3446.Gravatar Matthieu Sozeau2015-06-11
* STM: states coming from workers have no proof terminators (Close #4246)Gravatar Enrico Tassi2015-06-09
* STM: silly mistake in jumping back to an old state (Close #4249)Gravatar Enrico Tassi2015-06-09
* Adding a test for bug #4057.Gravatar Pierre-Marie Pédrot2015-06-02
* Flag -test-mode intended to be used for ad-hoc prints in test-suiteGravatar Enrico Tassi2015-05-29
* STM: preserve branch name on edit (Close: #4245, #4246)Gravatar Enrico Tassi2015-05-28
* Test for 4159Gravatar Enrico Tassi2015-05-28
* Test for bug #4116.Gravatar Pierre-Marie Pédrot2015-05-19
* Removing test for opened bugs that were already present in the closed test-su...Gravatar Pierre-Marie Pédrot2015-05-18
* Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Gravatar Pierre-Marie Pédrot2015-05-18
* Removing option -no-native-compiler from test #3539 since this option is nowGravatar Hugo Herbelin2015-05-15
* Fixing bug #4216:Gravatar Pierre-Marie Pédrot2015-05-13
* Better fixing #4198 such that the term to match is looked for beforeGravatar Hugo Herbelin2015-05-13
* Extraction: fix the detection of the "polyprop" situationGravatar Pierre Letouzey2015-05-12
* Test for bug #4234.Gravatar Pierre-Marie Pédrot2015-05-12
* Test for bug #4232.Gravatar Pierre-Marie Pédrot2015-05-11
* Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Gravatar Hugo Herbelin2015-05-09
* Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forGravatar Hugo Herbelin2015-05-09
* Fixing treatment of recursive equations damaged by 857e82b2ca0d1.Gravatar Hugo Herbelin2015-05-06
* Fixing computation of implicit arguments by position in fixpoints (#4217).Gravatar Hugo Herbelin2015-05-01
* Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Test for #4198 (appcontext in return clause of match).Gravatar Hugo Herbelin2015-04-22
* Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentGravatar Hugo Herbelin2015-04-21
* Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalGravatar Hugo Herbelin2015-04-17
* Test for bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* Test for bug #3199.Gravatar Pierre-Marie Pédrot2015-04-10
* Better test-suite files, removing reliance on admit.Gravatar Matthieu Sozeau2015-04-09
* Fix declarations of instances to perform restriction of universeGravatar Matthieu Sozeau2015-04-09
* Add test-suite file for bug #4120.Gravatar Matthieu Sozeau2015-04-09
* Test for bug #3815.Gravatar Pierre-Marie Pédrot2015-04-06
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-04-01
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-03-31
* camlp4: grep away warnings in output/* testsGravatar Enrico Tassi2015-03-30
* Adding test for bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Another example about the consequence of a wrong computation of theGravatar Hugo Herbelin2015-03-25
* Updating test-suite (see previous commit).Gravatar Hugo Herbelin2015-03-24
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22