| Age | Commit message (Expand) | Author |
|---|
| 2016-08-18 | Adding a test for bug #4653. | Pierre-Marie Pédrot |
| 2016-08-17 | Fixing #3070 ("subst" taking properly into account chains of dependencies). | Hugo Herbelin |
| 2016-08-16 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot |
| 2016-07-29 | Fix bug #4673: regression in setoid_rewrite. | Matthieu Sozeau |
| 2016-07-29 | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau |
| 2016-07-29 | Fix bug #3886, generation of obligations of fixes | Matthieu Sozeau |
| 2016-07-29 | Fix #4769, univ poly and elim schemes in sections | Matthieu Sozeau |
| 2016-07-26 | Fix bug #4754, allow conversion problems to remain | Matthieu Sozeau |
| 2016-07-21 | Fix bug #4679, weakened setoid_rewrite unification | Matthieu Sozeau |
| 2016-07-20 | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau |
| 2016-07-20 | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau |
| 2016-07-18 | A new step on using alpha-conversion in printing notations. | Hugo Herbelin |
| 2016-07-18 | Marking bug #3383 as solved. | Pierre-Marie Pédrot |
| 2016-07-18 | Fix bug #4923: Warning: appcontext is deprecated. | Pierre-Marie Pédrot |
| 2016-07-17 | Fixing #4932 (anomaly when using binders as terms in recursive notations). | Hugo Herbelin |
| 2016-07-13 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot |
| 2016-07-08 | Fix test file for #4858. | Maxime Dénès |
| 2016-07-08 | Test file for #4858. | Maxime Dénès |
| 2016-07-08 | Add test file for #4880. | Maxime Dénès |
| 2016-07-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot |
| 2016-07-07 | Merge remote-tracking branch 'github/bug4653' into v8.6 | Matthieu Sozeau |
| 2016-07-07 | Program: fix #4873: transparency option not used | Matthieu Sozeau |
| 2016-07-06 | Fixed bug #4622. | Matthieu Sozeau |
| 2016-07-06 | Merge remote-tracking branch 'github/pr/199' into v8.5 | Maxime Dénès |
| 2016-07-06 | Fix test-suite file 3690 | Matthieu Sozeau |
| 2016-07-05 | congruence fix: test-suite code and update CHANGES | Matthieu Sozeau |
| 2016-07-04 | Merge branch 'v8.5' into trunk | Maxime Dénès |
| 2016-07-04 | congruence/univs: properly refresh (fix #4609) | Matthieu Sozeau |
| 2016-07-02 | Adding test for #4811. | Hugo Herbelin |
| 2016-07-01 | Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars). | Hugo Herbelin |
| 2016-06-29 | Fixing #4865 (deciding on which arguments to recompute scopes was not robust). | Hugo Herbelin |
| 2016-06-29 | Univs: Fix bug #4726 | Matthieu Sozeau |
| 2016-06-29 | Fix issues in test-suite revealed by warnings. | Maxime Dénès |
| 2016-06-27 | Univs: allowing notations to take univ instances | Matthieu Sozeau |
| 2016-06-27 | Forbidding silently dropped universes instances in | Matthieu Sozeau |
| 2016-06-27 | Shrink Proofs/Obligations by default and deprecate | Matthieu Sozeau |
| 2016-06-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-06-27 | More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause). | Hugo Herbelin |
| 2016-06-18 | Giving a more natural semantics to injection by default. | Hugo Herbelin |
| 2016-06-16 | Refine 9cc95f5, unification of Let-In's, bug #3929 | Matthieu Sozeau |
| 2016-06-15 | Fix test-suite for opened bug #4813. | Pierre-Marie Pédrot |
| 2016-06-14 | Merge branch 'bug4450' into v8.5 | Matthieu Sozeau |
| 2016-06-14 | Merge branch 'bug4725' into v8.5 | Matthieu Sozeau |
| 2016-06-14 | Admitted: fix #4818 return initial stmt and univs | Matthieu Sozeau |
| 2016-06-13 | Univs: more robust Universe/Constraint decls #4816 | Matthieu Sozeau |
| 2016-06-13 | Fix test-suite file, only part 2 is fixed in 8.5 | Matthieu Sozeau |
| 2016-06-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-06-13 | Univs: fix for part #2 of bug #4816. | Matthieu Sozeau |
| 2016-06-12 | For the record, an example one would like to see working. | Hugo Herbelin |
| 2016-06-12 | Another fix to #4782 (a typing error not captured when dealing with bindings). | Hugo Herbelin |
