aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
* Test file for #3948 - Anomaly: unknown constant in Print Assumptions.Gravatar Maxime Dénès2015-09-20
* In pat/constr introduction patterns, fixing in a better way clearing problemsGravatar Hugo Herbelin2015-09-16
* Test for bug #4269.Gravatar Pierre-Marie Pédrot2015-09-15
* STM: Reset takes Ltac <ident> into account (Close #4316)Gravatar Enrico Tassi2015-09-15
* Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsGravatar Hugo Herbelin2015-09-08
* Ensuring that patterns of the form pat/constr move the hypotheses replacingGravatar Hugo Herbelin2015-09-08
* Update test-suite after 518049fe7.Gravatar Maxime Dénès2015-09-03
* Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Gravatar Hugo Herbelin2015-08-21
* Test file for #4254: Mutual inductives with parameters on Type raises anomaly.Gravatar Maxime Dénès2015-08-03
* Continuing 817308ab (use ltac env for terms in ltac context) + fixGravatar Hugo Herbelin2015-08-02
* Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
* Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
* Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Test file for bug #4289 (buggy hash-consing of kernel name pairsGravatar Hugo Herbelin2015-07-30
* Adding test for bug #3779.Gravatar Pierre-Marie Pédrot2015-07-29
* Adding a test for bug #4280.Gravatar Pierre-Marie Pédrot2015-07-28
* Updating test-suite for #3510.Gravatar Pierre-Marie Pédrot2015-07-28
* Tests for bugs #3509 and #3510.Gravatar Pierre-Marie Pédrot2015-07-28
* Test for bug #2243.Gravatar Pierre-Marie Pédrot2015-07-27
* Fixing #4305 (compatibility wrt 8.4 in not interpreting anGravatar Hugo Herbelin2015-07-27
* Fixing bug #3736 (anomaly instead of error/warning/silence onGravatar Hugo Herbelin2015-07-27
* Output test for bug #2169.Gravatar Pierre-Marie Pédrot2015-07-27
* test-suite: add test for bug# 3743.Gravatar Matthieu Sozeau2015-07-22
* Extraction: fix primitive projection extraction.Gravatar Matthieu Sozeau2015-07-22
* Refining 71def2f8 on too strong occur-check limiting evar-evarGravatar Hugo Herbelin2015-07-16
* Remove old test file for #3819 (now fixed).Gravatar Maxime Dénès2015-07-16
* Fixing bug #4240 (closure_of_filter was not ensuring refinement ofGravatar Hugo Herbelin2015-07-16
* Test file for #3819.Gravatar Maxime Dénès2015-07-16
* Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
* Kernel: primitive projections handling of let-insGravatar Matthieu Sozeau2015-07-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 15:08:22 +0000