| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
The Software Foundations archive has been replaced by three volumes.
|
|
|
|
For some reason, OPAM was not happy after we reinstalled curl.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
implementation from Detyping.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
With a minimal diff (so I'm not putting quotes ` ` around all the code).
|
|
|
|
|
|
This is a temporary workaround, until we fix the underlying issue which
makes coqtop hang on those tests.
|
|
|
|
The code generating the projection was unconditionally generating
pattern-matchings, although this is incorrect for primitive records.
|
|
|
|
|
|
|
|
|
|
|
|
restructuration
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
