aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
Commit message (Expand)AuthorAge
* Univs: fixed 3685 by side-effect :)Gravatar Matthieu Sozeau2015-10-02
* Univs: minor fixes to test-suite filesGravatar Matthieu Sozeau2015-10-02
* Univs: fix test-suite file for HoTT/coq bug #120Gravatar Matthieu Sozeau2015-10-02
* Univs: test-suite file for bug #2016Gravatar Matthieu Sozeau2015-10-02
* Univs: test-suite file for #4301, subtyping of poly parametersGravatar Matthieu Sozeau2015-10-02
* Fix test-suite file for bug #3777Gravatar Matthieu Sozeau2015-10-02
* Fix test-suite file: failing earlier as expected.Gravatar Matthieu Sozeau2015-10-02
* Univs: fixed bug 2584, correct universe found for mutual inductive.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix Universe vernacular, fix bug #4287.Gravatar Matthieu Sozeau2015-10-02
* Univs: fixed bug #4328.Gravatar Matthieu Sozeau2015-10-02
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* Test for bug #4347.Gravatar Pierre-Marie Pédrot2015-09-26
* Test file for #3948 - Anomaly: unknown constant in Print Assumptions.Gravatar Maxime Dénès2015-09-20
* STM: Reset takes Ltac <ident> into account (Close #4316)Gravatar Enrico Tassi2015-09-15
* 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
* Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
* 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
* test-suite: add test for bug# 3743.Gravatar Matthieu Sozeau2015-07-22
* Refining 71def2f8 on too strong occur-check limiting evar-evarGravatar Hugo Herbelin2015-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
* 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 bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Add test-suite file for bug #3446.Gravatar Matthieu Sozeau2015-06-11
* Adding a test for bug #4057.Gravatar Pierre-Marie Pédrot2015-06-02
* Test for bug #4116.Gravatar Pierre-Marie Pédrot2015-05-19
* 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
* Test for bug #4234.Gravatar Pierre-Marie Pédrot2015-05-12
* Test for bug #4232.Gravatar Pierre-Marie Pédrot2015-05-11
* Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forGravatar Hugo Herbelin2015-05-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 03:23:12 +0000