lp:~jgross-h/coq/v8.5
- Get this branch:
- bzr branch lp:~jgross-h/coq/v8.5
Branch merges
Branch information
Import details
This branch is an import of the HEAD branch of the Git repository at https://github.com/coq/coq.git,branch=v8.5.
Last successful import was .
Recent revisions
- 18522. By Hugo Herbelin <email address hidden>
-
Fixing unification regression #5323.
Tracking conversion problems to reconsider was lost for evars subject
to restriction (field last_mods was not updated and conversion
problems not considered to be changed). - 18521. By Hugo Herbelin <email address hidden>
-
Fixing a little bug in printing cofix with no arguments.
- 18520. By Guillaume Melquiond <email address hidden>
-
Handle application of a primitive projection to a not yet evaluated cofixpoint (bug #5286).
- 18519. By Guillaume Melquiond <email address hidden>
-
Fix broken documentation in presence of \zeroone{... \tt ...}.
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. - 18516. By Guillaume Melquiond <email address hidden>
-
Remove spurious spaces in merlin file generated by coq_makefile (bug #5213).
- 18515. By Hugo Herbelin <email address hidden>
-
Excluding explicitly coinductive types in Scheme Equality (#5284).
- 18513. By Hugo Herbelin <email address hidden>
-
Fixing #5161 (case of a notation with unability to detect a recursive binder).
Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.
Branch metadata
- Branch format:
- Branch format 7
- Repository format:
- Bazaar repository format 2a (needs bzr 1.16 or later)