| Commit message (Collapse) | Author | Age |
... | |
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
| | | | | | | | | |
|
| |_|_|_|/ / / /
|/| | | | | | | |
|
| |_|_|_|_|/ /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
Currently, `make ci-sf` downloads and builds the files in the main root
directory. we fix that.
|
| | | | | | |
|
|\ \ \ \ \ \ |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Closes #6194 .
|
|\ \ \ \ \ \ \
| |_|/ / / / /
|/| | | | | | |
|
| |_|_|/ / /
|/| | | | | |
|
| |_|_|/ /
|/| | | | |
|
| | | | | |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| |/ / / / /
|/| | | | | |
|
|\ \ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| |_|/ / / /
|/| | | | |
| | | | | |
| | | | | | |
Was still relying on the existence of user-configured /pr/.
|
| | | |/ /
| | |/| |
| | | | |
| | | | |
| | | | | |
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
|
| |_|_|/
|/| | | |
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We remove the progs target [examples] to save time, we still build the
full library thou.
I guess we can't do better for now unless we get some Travis
subscription.
|
|\ \ \ |
|
| |/ / |
|
|\ \ \ |
|
|\ \ \ \
| |_|/ /
|/| | | |
|
| | | | |
|
|\ \ \ \
| |_|_|/
|/| | | |
|
| |/ /
|/| |
| | |
| | |
| | | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| |/
|/| |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
| |_|_|/
|/| | | |
|
| |_|/
|/| | |
|
|\ \ \ |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
|
| |/
|/|
| |
| |
| |
| | |
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
|\ \ |
|
|\ \ \ |
|
| | | | |
|
|\ \ \ \ |
|
|\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| |_|/ /
|/| | | |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to
put any pattern in binders, prefixed by a quote."] its current
placement as well as the hook don't make a lot of sense.
In particular, they prevent parts of Coq working without linking the
parser.
To this purpose, we need to consolidate the `Constrexpr`
utilities. While we are at it we do so and remove the `Topconstr`
module which is fully redundant with `Constrexpr_ops`.
|