| Age | Commit message (Collapse) | Author |
|---|
|
packaging
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
|
|
|
|
Parameters)
Reviewed-by: Matafou
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Ex: "(tactic)" instead of "(tacn)"
|
|
There is not need for coqdep to ship an `ocamldep` replacement, in
particular:
- not used in the main build since a long time
- not tested
- not kept up to date with upstream
This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.
`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.
We also remove the residual `-slash` option.
|
|
They are always used together, no other use case of `-suffix` that I
can see.
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
beta versions.
Reviewed-by: ejgallego
|
|
missing them.
Reviewed-by: ejgallego
|
|
`theories` now never have `.ml` files inside.
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
Ack-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: maximedenes
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
This was already possible manually using "{ _ }" in the type of
declaration. This was also possible for type classes. So, no reason to
forbid in Arguments.
|
|
|
|
Reviewed-by: ejgallego
|
|
No reason to have them in the same .sh
|
|
In previous refactorings `vernac_loop` stopped being tail-recursive,
we refactor code a bit and make it back into tail-recursive form.
|
|
We refactor control loop a bit to make the code more readable:
- the code for unhandled exception is not needed anymore as it cannot
happen.
- we move the processing of toplevel commands to its own function
- we split away diff-specific functions.
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Reviewed-by: ppedrot
|
|
and cofix
Reviewed-by: SkySkimmer
|
|
|
|
Instead of various termops and globnames aliases.
|
|
The previous system was from before globref was in the kernel.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
The interpreter directive of “doc/stdlib/make-library-index” must be patched.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: vbgl
|
|
|
|
Motivations:
- We should have only maintained developments in our CI
- `make ci-fiat-crypto-legacy` takes about 15 mins before the first call
to `coqc`, making it unusable to work on overlays
- The coding style of this development is so fragile that adapting to
any change of behavior requires diffing gigabytes of Ltac traces.
@mattam82 and I have been blocked for 6 months this way, when working on
unifall.
I understand this development was meant to stress-test some components
like printing, but I think the trade-off is bad. We should rather come
up with specialized test suites for these components.
|
|
|
|
- Implicit arguments in the return clause and in the branches
of a match were not checked.
- Implicit arguments in each declaration of intern_context were not
restarted.
- Additionally, in intern_context, we take into account ids from the
env on top of which intern_context is called.
- A better approximation of the check for manual implicit in notations
improved (though not fully correct because the exact context of
interpretation of a binder in a notation with recursive binders is
not known).
We also rename impl_binder_index into binder_block_names in anticipation of
checking redundancies also for non-implicit arguments.
|
