Coq

lp:~jgross-h/coq/v8.5

Created by Jason Gross and last modified
Get this branch:
bzr branch lp:~jgross-h/coq/v8.5

Branch merges

Related bugs

Related blueprints

Branch information

Owner:
Jason Gross
Project:
Coq
Status:
Development

Import details

Import Status: Failed

This branch is an import of the HEAD branch of the Git repository at https://github.com/coq/coq.git,branch=v8.5.

The import has been suspended because it failed 5 or more times in succession.

Last successful import was .

Import started on pear and finished taking 40 seconds — see the log
Import started on pear and finished taking 40 seconds — see the log
Import started on pear and finished taking 40 seconds — see the log
Import started on pear and finished taking 40 seconds — see the log

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.

18518. By Guillaume Melquiond <email address hidden>

Update documentation (bugs #5246 and #5251).

18517. By Guillaume Melquiond <email address hidden>

Fix some documentation typos.

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).

18514. By Hugo Herbelin <email address hidden>

Fixing anomaly EqUnknown in Equality Scheme (#5278).

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)
This branch contains Public information 
Everyone can see this information.

Subscribers