aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Avoid using the deprecated Scanf.fscanf function.Gravatar Maxime Dénès2017-01-09
|
* OCaml's -dtypes flag is deprecated and replaced by -annot.Gravatar Maxime Dénès2017-01-09
|
* Relax required OCaml to 4.02.1.Gravatar Maxime Dénès2017-01-09
| | | | | | We did not decide precisely what minor version we would support, so relaxing. We document why 4.02.0 is not supported (its use is also discouraged by the OCaml team, see e.g. https://ocaml.org/releases/).
* Merge remote-tracking branch 'github/pr/350' into trunkGravatar Maxime Dénès2017-01-09
|\ | | | | | | Was PR#350: tclDISPATCH: more informative error message
* | Fixing #5277 (Scheme Equality not robust wrt choice of names).Gravatar Hugo Herbelin2016-12-22
| | | | | | | | This is only a quick fix, as hinted by Jason.
* | Fixing injection in the presence of let-in in constructors.Gravatar Hugo Herbelin2016-12-22
| | | | | | | | This also fixes decide equality, discriminate, ... (see e.g. #5279).
* | Merge remote-tracking branch 'github/pr/172' into trunkGravatar Maxime Dénès2016-12-19
|\ \ | | | | | | | | | Was PR#172: alternate path separators in typeclass debug output.
* \ \ Merge remote-tracking branch 'github/pr/351' into trunkGravatar Maxime Dénès2016-12-19
|\ \ \ | | | | | | | | | | | | Was PR#351: Complete a truncated comment
* \ \ \ Merge remote-tracking branch 'github/pr/363' into trunkGravatar Maxime Dénès2016-12-19
|\ \ \ \ | | | | | | | | | | | | | | | Was PR#363: lib/Unicodetable: Update.
* | | | | Fix a typo in Hurkens.v commentGravatar Jason Gross2016-12-19
| | | | |
* | | | | Bump required OCaml version to 4.02.3.Gravatar Maxime Dénès2016-12-19
| | | | | | | | | | | | | | | | | | | | Was decided during the working group on September, 28th.
* | | | | Use Pp.quote in string options.Gravatar Maxime Dénès2016-12-19
| | | | |
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\ \ \ \ \
| * | | | | Fix #5248 - test-suite fails in 8.6beta1Gravatar Maxime Dénès2016-12-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was yet another bug in the VM long multiplication, that I unfortunately introduced in ebc509ed2. It was impacting only 32-bit architectures. In the future, I'll try to make sure that 1) we provide unit tests for integer arithmetic (my int63 branch ships with such tests) 2) our continuous testing infrastructure runs the test suite on a 32-bit architecture. I tried to set up such an instance, but failed. Waiting for support reply.
| * | | | | Fix broken documentation in presence of \zeroone{... \tt ...}.Gravatar Guillaume Melquiond2016-12-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there.
| * | | | | Update documentation (bugs #5246 and #5251).Gravatar Guillaume Melquiond2016-12-06
| | | | | |
| * | | | | Merge remote-tracking branch 'github/pr/387' into v8.6Gravatar Maxime Dénès2016-12-06
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#387: ssrmatching: handle primitive projections (fix: #5247)
| * \ \ \ \ \ Merge remote-tracking branch 'github/pr/389' into v8.6Gravatar Maxime Dénès2016-12-06
| |\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#389: Changed mention of deprecated -byte option to .byte suffix; change module for Coq loop
| | * | | | | | Change module for Coq loopGravatar Paul Steckler2016-12-05
| | | | | | | |
| | * | | | | | the -byte option is deprecatedGravatar Paul Steckler2016-12-05
| |/ / / / / /
| | * | | | | ssrmatching: handle primite projections (fix: #5247)Gravatar Enrico Tassi2016-12-05
| | | | | | |
| * | | | | | Compute dependency of C files only in kernel/byterun.Gravatar Maxime Dénès2016-12-05
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Some C files included in build scripts (in dev/build) were triggering errors or warnings on non-win32 platforms. Note that ide/ide_win32_stubs.c was already handled through an ad-hoc rule in Makefile. If you add a new C file outside of kernel/byterun, please extend the CFILES variable.
| * | | | | Merge remote-tracking branch 'github/pr/366' into v8.6Gravatar Maxime Dénès2016-12-04
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#366: Univs: fix bug 5208
| * \ \ \ \ \ Merge remote-tracking branch 'github/pr/378' into v8.6Gravatar Maxime Dénès2016-12-04
| |\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | Was PR#378: Univs: fix bug #5188
| * | | | | | | Fix test-suite after change in "context" printing.Gravatar Maxime Dénès2016-12-02
| | | | | | | |
| | | * | | | | Document changesGravatar Matthieu Sozeau2016-12-02
| | | | | | | |
| * | | | | | | Merge remote-tracking branch 'github/pr/377' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#377: Univs: fix bug #5180
| * \ \ \ \ \ \ \ Merge remote-tracking branch 'github/pr/372' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'github/pr/368' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#368: Add example in dev/doc/changes involving Tacmach.project
| * \ \ \ \ \ \ \ \ \ Merge branch 'pr/367' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Parts of PR#367: Fixing the "beautifier" and checking the parsing-printing reversibility
| | * | | | | | | | | | Fixing lexing of strings in comments for beautifier.Gravatar Hugo Herbelin2016-12-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was a bug introduced in 0ad6edc1.
| | * | | | | | | | | | Fixing printing of "ltac:" in tactics after surrounding parenthesesGravatar Hugo Herbelin2016-12-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | became mandatory.
| | | | | | * | | | | | Comment on universe handling in ParametersGravatar Matthieu Sozeau2016-12-02
| | | | | | | | | | | |
| | | | | | * | | | | | Univs: fix bug #5188Gravatar Matthieu Sozeau2016-12-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Parameter was implemented the wrong way trying to separate the universes of the telescope.
| * | | | | | | | | | | Merge remote-tracking branch 'github/pr/381' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#381: V8.6+fix typeclasses eauto shelving
| * | | | | | | | | | | | Fix #5242 - Dubious unsilenceable warning on invalid identifierGravatar Maxime Dénès2016-12-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make this warning configurable and disabled by default.
| | | * | | | | | | | | | Fixing printing of "Set Warnings Append".Gravatar Hugo Herbelin2016-12-02
| | | | | | | | | | | | |
| | | * | | | | | | | | | Fixing space in printing "Context".Gravatar Hugo Herbelin2016-12-02
| | | | | | | | | | | | |
| | | * | | | | | | | | | Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-12-02
| | | | | | | | | | | | |
| | | * | | | | | | | | | Fixing space in printing several list of implicit arguments.Gravatar Hugo Herbelin2016-12-02
| | | | | | | | | | | | |
| | | * | | | | | | | | | Fixing printing of "only parsing" in abbreviations.Gravatar Hugo Herbelin2016-12-02
| | | | | | | | | | | | |
| | | * | | | | | | | | | Protect printing of ltac's "context [...]" from possible collisionGravatar Hugo Herbelin2016-12-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | with user-level notations by inserting spaces.
| | | * | | | | | | | | | More on fixing #5098 (preserving printing of "in hyp").Gravatar Hugo Herbelin2016-12-02
| | |/ / / / / / / / / / | |/| | | | | | | | | |
| * | | | | | | | | | | Merge remote-tracking branch 'github/pr/380' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#380: Fix bug #5232: proper globalization of hints paths
| * \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'github/pr/369' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#369: Make a note about wit_constr and Constrarg in dev/doc/changes
| * \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'github/pr/371' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#371: Update dev/doc/changes with things about mem_named_context
| * \ \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'github/pr/364' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#364: Add missing label. Fixes broken ref.
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'github/pr/382' into v8.6Gravatar Maxime Dénès2016-12-02
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#382: [merlin] Adjust merlin for ide.
| | * | | | | | | | | | | | | | | [merlin] Adjust merlin for ide.Gravatar Emilio Jesus Gallego Arias2016-11-30
| |/ / / / / / / / / / / / / / /
* | | | | | | | | | | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\| | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:19:14 +0000