aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Bug Fixes : 4851 4858 4880 for nsatzGravatar thery2016-07-06
* Prevent unsafe overwriting of Required modules by toplevel library.Gravatar Maxime Dénès2016-07-05
* congruence fix: test-suite code and update CHANGESGravatar Matthieu Sozeau2016-07-05
* Pass .v files to coqc in Makefile produced by coq_makefile (bug #4896).Gravatar Guillaume Melquiond2016-07-05
* Add mailmap entry.Gravatar Guillaume Melquiond2016-07-05
* Bug fix : variable capture in ltac code of NsatzGravatar thery2016-07-05
* Merge branch 'congruencefix' into v8.5Gravatar Matthieu Sozeau2016-07-04
|\
| * congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
| * congruence: remove casts of indexed termsGravatar Matthieu Sozeau2016-07-04
| * congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
* | Mention more fixes in CHANGES before we release pl2.Gravatar Maxime Dénès2016-07-04
* | Revert "Improve the interpretation scope of arguments of an ltac match."Gravatar Maxime Dénès2016-07-04
|/
* test-suite: test checking of libraries checksum.Gravatar Maxime Dénès2016-07-04
* Merge remote-tracking branch 'github/pr/228' into v8.5Gravatar Maxime Dénès2016-07-04
|\
* | Fixing use of "Declare Implicit Tactic" in refine.Gravatar Hugo Herbelin2016-07-01
* | Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).Gravatar Hugo Herbelin2016-07-01
* | Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).Gravatar Hugo Herbelin2016-07-01
| * fix coqide double module linking (error on OCaml 4.03)Gravatar Gabriel Scherer2016-06-28
|/
* Merge branch 'forhott' into v8.5Gravatar Matthieu Sozeau2016-06-28
|\
| * Univs/CHANGES: #4097 and annotations on notationsGravatar Matthieu Sozeau2016-06-27
| * Refine fix for bug #4097, avoid proj expansionGravatar Matthieu Sozeau2016-06-27
| * Univs: allowing notations to take univ instancesGravatar Matthieu Sozeau2016-06-27
| * Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
|/
* More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Gravatar Hugo Herbelin2016-06-27
* Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies.Gravatar Pierre-Marie Pédrot2016-06-27
* Fix typo.Gravatar Guillaume Melquiond2016-06-23
* Remove extraction-specific code from the checker.Gravatar Guillaume Melquiond2016-06-23
* Reference Manual / Extraction: the original example command no longer works w...Gravatar Matej Kosik2016-06-20
* A hack to fix another regression with Ltac trace report in 8.5. E.g.Gravatar Hugo Herbelin2016-06-18
* remote counter: avoid thread race on sockets (fix #4823)Gravatar Enrico Tassi2016-06-17
* Merge branch 'bug4450' into v8.5Gravatar Matthieu Sozeau2016-06-14
|\
* \ Merge branch 'bug4725' into v8.5Gravatar Matthieu Sozeau2016-06-14
|\ \
* | | Admitted: fix #4818 return initial stmt and univsGravatar Matthieu Sozeau2016-06-14
* | | Fix test-suite file, only part 2 is fixed in 8.5Gravatar Matthieu Sozeau2016-06-13
* | | Univs: fix for part #2 of bug #4816.Gravatar Matthieu Sozeau2016-06-13
* | | evar_conv: Refine occur_rigidlyGravatar Matthieu Sozeau2016-06-13
* | | Tentatively fixing misguiding error message with "binder" type inGravatar Hugo Herbelin2016-06-13
* | | Minor simplification in evarconv.Gravatar Hugo Herbelin2016-06-12
* | | Another fix to #4782 (a typing error not captured when dealing with bindings).Gravatar Hugo Herbelin2016-06-12
* | | Reserve exception "ConversionFailed" in unification for failure ofGravatar Hugo Herbelin2016-06-12
* | | Protecting eta-expansion in evarconv.ml against ill-typed problems.Gravatar Hugo Herbelin2016-06-12
* | | Fixing bug in printing CannotSolveConstraint (collision of context names).Gravatar Hugo Herbelin2016-06-12
* | | Fixing #4782 (a typing error not captured when dealing with bindings).Gravatar Hugo Herbelin2016-06-11
* | | Fixing a try with in apply that has become too weak in 8.5.Gravatar Hugo Herbelin2016-06-11
* | | Reporting about a few bug fixes (to be continued).Gravatar Hugo Herbelin2016-06-09
* | | Fixing #4644 (regression of unification on evar-evar problems with a match).Gravatar Hugo Herbelin2016-06-09
* | | Minor simplification in evarconv.ml.Gravatar Hugo Herbelin2016-06-09
* | | New update on how to find camlp5 binary and library at configure time.Gravatar Hugo Herbelin2016-06-09
* | | Improve the interpretation scope of arguments of an ltac match.Gravatar Hugo Herbelin2016-06-09
* | | Reverting dbdff037 which does not seem to prevent to have #3638 fixedGravatar Hugo Herbelin2016-06-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 03:35:38 +0000