| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.
We know split the directory in two, as to make the distinction clear:
- `clib`: contains libraries that are not Coq specific and implement
common data structures and programming patterns. These libraries
could be eventually replace with external dependencies and the rest
of the code base wouldn't notice much.
- `lib`: contains Coq-specific common libraries in widespread use
along the codebase, but that are not considered part of other
components. Examples are printing, error handling, or flags.
In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.
Also note that `Deque` is not used ATM.
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
| |
Now it is a private field, locations are optional.
|
| |
|
|
|
|
|
|
| |
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
| |
|
|
|
|
|
|
|
| |
We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.
- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
| |
together with the tactic monad.
The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
I added a .merlin in ide/ who inherits everything from the root .merlin and also
adds the dependency to lablgtk, which I removed from the root file. These way
people not working on that part of the code won't get bothered if they don't
have that package.
I removed the S/B entry for plugins which was useless, indeed there is no ML
file in that directory and merlin doesn't scan the subdirectories recursively
(as you know).
I also removed the S/B entry for checker since most of the files of this
directory are also present in kernel and that was the cause of a lot errors on
merlin's side (think "inconsistent assumptions").
On top of that, no part of the tree depends on checker (I back that assertion by
a grep of the *.d files of the tree) so these lines in the .merlin were actually
useless. The only part of the tree where you need to know what's in checker/ is
when you are working in checker/ itself, but since merlin automatically adds the
directory of the file under edition in its source and load paths nothing else is
needed.
There might still be problems after this patch, but they should be less of them.
Considering my poor knowledge of the codebase there might be other conflicts I
have missed.
|
| | |
|
| | |
|
| |
|
Emilio Jesus Gallego Arias
Matej Kosik
Maxime Dénès
Gaetan Gilbert
Pierre-Marie Pédrot
Thomas Refis
Pierre Boutillier