| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Reviewed-by: MSoegtropIMC
|
|
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
Integrate merging doc in the main contributing document.
|
|
Reviewed-by: ejgallego
|
|
- remove manual flexlink circular dependency handling
- use standard configure process instead of hand made windows make files
- enable parallel build
- remove bootstrapping step (maybe should be there for release builds)
|
|
We restrict to those that are actually related to typeclasses, and
perform the following renamings:
Classops --> Coercionops
Class --> ComCoercion
|
|
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
INSTALL.md
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: jfehrle
|
|
|
|
|
|
|
|
For now we don't enable it in any source file, neither on dune files.
`lint-repository` has been updated so it will check `dune build @fmt`
returns 0.
|
|
|
|
|
|
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
Reviewed-by: Zimmi48
|
|
|
|
This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.
Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.
|
|
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
It seems we need to pass the token to the actual artifact download.
|
|
|
|
It is useful for the release process, and there is no reason for somebody
to lose time reimplementing it again.
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
|
|
This adds a couple extra files, but not many.
|
|
|
|
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
|
|
c.f. https://github.com/coq/coq/pull/11032#issue-335944369
Also, change the default from python2 to python3 for update-compat while
we're at it, and update file unicode handling accordingly.
(Note that this file still works with both python2 and python3.)
|
|
thanks
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
|
|
|
|
is fixed
Reviewed-by: Zimmi48
|
|
(by the checker refactor AFAICT)
+ fix commit for the coqtop side fix (it got rebased at some point)
Close #10705
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
Reviewed-by: Zimmi48
|
|
|
|
* This commit add float instructions to the VM, their encoding in bytecode
and the interpretation of primitive float values after the reduction.
* The flag '-std=c99' could be added to the C compiler flags to ensure
that float computation strictly follows the norm (ie. i387 80-bits
format is not used as an optimization).
Actually, we use '-fexcess-precision=standard' instead of '-std=c99'
because the latter would disable GNU asm used in the VM.
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
Reviewed-by: SkySkimmer
|
