aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-12-22Fixing #5277 (Scheme Equality not robust wrt choice of names).Hugo Herbelin
This is only a quick fix, as hinted by Jason.
2016-12-22Fixing injection in the presence of let-in in constructors.Hugo Herbelin
This also fixes decide equality, discriminate, ... (see e.g. #5279).
2016-12-19Merge remote-tracking branch 'github/pr/172' into trunkMaxime Dénès
Was PR#172: alternate path separators in typeclass debug output.
2016-12-19Merge remote-tracking branch 'github/pr/351' into trunkMaxime Dénès
Was PR#351: Complete a truncated comment
2016-12-19Merge remote-tracking branch 'github/pr/363' into trunkMaxime Dénès
Was PR#363: lib/Unicodetable: Update.
2016-12-19Fix a typo in Hurkens.v commentJason Gross
2016-12-19Bump required OCaml version to 4.02.3.Maxime Dénès
Was decided during the working group on September, 28th.
2016-12-19Use Pp.quote in string options.Maxime Dénès
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-06Fix #5248 - test-suite fails in 8.6beta1Maxime Dénès
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.
2016-12-06Fix broken documentation in presence of \zeroone{... \tt ...}.Guillaume Melquiond
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.
2016-12-06Update documentation (bugs #5246 and #5251).Guillaume Melquiond
2016-12-06Merge remote-tracking branch 'github/pr/387' into v8.6Maxime Dénès
Was PR#387: ssrmatching: handle primitive projections (fix: #5247)
2016-12-06Merge remote-tracking branch 'github/pr/389' into v8.6Maxime Dénès
Was PR#389: Changed mention of deprecated -byte option to .byte suffix; change module for Coq loop
2016-12-05Change module for Coq loopPaul Steckler
2016-12-05the -byte option is deprecatedPaul Steckler
2016-12-05ssrmatching: handle primite projections (fix: #5247)Enrico Tassi
2016-12-05Compute dependency of C files only in kernel/byterun.Maxime Dénès
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.
2016-12-04Merge remote-tracking branch 'github/pr/366' into v8.6Maxime Dénès
Was PR#366: Univs: fix bug 5208
2016-12-04Merge remote-tracking branch 'github/pr/378' into v8.6Maxime Dénès
Was PR#378: Univs: fix bug #5188
2016-12-02Fix test-suite after change in "context" printing.Maxime Dénès
2016-12-02Document changesMatthieu Sozeau
2016-12-02Merge remote-tracking branch 'github/pr/377' into v8.6Maxime Dénès
Was PR#377: Univs: fix bug #5180
2016-12-02Merge remote-tracking branch 'github/pr/372' into v8.6Maxime Dénès
Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes
2016-12-02Merge remote-tracking branch 'github/pr/368' into v8.6Maxime Dénès
Was PR#368: Add example in dev/doc/changes involving Tacmach.project
2016-12-02Merge branch 'pr/367' into v8.6Maxime Dénès
Parts of PR#367: Fixing the "beautifier" and checking the parsing-printing reversibility
2016-12-02Fixing lexing of strings in comments for beautifier.Hugo Herbelin
Was a bug introduced in 0ad6edc1.
2016-12-02Fixing printing of "ltac:" in tactics after surrounding parenthesesHugo Herbelin
became mandatory.
2016-12-02Comment on universe handling in ParametersMatthieu Sozeau
2016-12-02Univs: fix bug #5188Matthieu Sozeau
Parameter was implemented the wrong way trying to separate the universes of the telescope.
2016-12-02Merge remote-tracking branch 'github/pr/381' into v8.6Maxime Dénès
Was PR#381: V8.6+fix typeclasses eauto shelving
2016-12-02Fix #5242 - Dubious unsilenceable warning on invalid identifierMaxime Dénès
We make this warning configurable and disabled by default.
2016-12-02Fixing printing of "Set Warnings Append".Hugo Herbelin
2016-12-02Fixing space in printing "Context".Hugo Herbelin
2016-12-02Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-12-02Fixing space in printing several list of implicit arguments.Hugo Herbelin
2016-12-02Fixing printing of "only parsing" in abbreviations.Hugo Herbelin
2016-12-02Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
with user-level notations by inserting spaces.
2016-12-02More on fixing #5098 (preserving printing of "in hyp").Hugo Herbelin
2016-12-02Merge remote-tracking branch 'github/pr/380' into v8.6Maxime Dénès
Was PR#380: Fix bug #5232: proper globalization of hints paths
2016-12-02Merge remote-tracking branch 'github/pr/369' into v8.6Maxime Dénès
Was PR#369: Make a note about wit_constr and Constrarg in dev/doc/changes
2016-12-02Merge remote-tracking branch 'github/pr/371' into v8.6Maxime Dénès
Was PR#371: Update dev/doc/changes with things about mem_named_context
2016-12-02Merge remote-tracking branch 'github/pr/364' into v8.6Maxime Dénès
Was PR#364: Add missing label. Fixes broken ref.
2016-12-02Merge remote-tracking branch 'github/pr/382' into v8.6Maxime Dénès
Was PR#382: [merlin] Adjust merlin for ide.
2016-11-30[merlin] Adjust merlin for ide.Emilio Jesus Gallego Arias
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-30Fix shelving order in typeclasses eauto.Théo Zimmermann
Before this fix, unshelve typeclasses eauto would produce sub-goals in the reverse order compared to when they were first shelved.
2016-11-30Fix typeclasses eauto shelving.Théo Zimmermann
A file in the test-suite had to be modified. It was supposed to reproduce a behavior in intuistionistic-nuprl but it did not really. This commit is not supposed to break intuistionistic-nuprl.
2016-11-30Fix bug #5232: proper globalization of hints pathsMatthieu Sozeau
2016-11-30Univs: fix bug #5180Matthieu Sozeau
In the kernel's generic conversion, backtrack on UniverseInconsistency for the unfolding heuristic (single backtracking point in reduction). This exception can be raised in the univ_compare structure to produce better error messages when the generic conversion function is called from higher level code in reductionops.ml, which itself is called during unification in evarconv.ml. Inside the kernel, the infer and check variants of conversion never raise UniverseInconsistency though, so this does not change the behavior of the kernel.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 18:04:58 +0000