| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
|
| |
We make math-comp overlays easier, we also start structuring the
scripts a bit more.
|
|\ |
|
| |
| |
| |
| |
| | |
Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15
minutes which is too much for Travis. Pity, because it was a nice use case.
|
|/ |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
This is a modest contribution serving before all the purpose of
displaying the focus stack and the shelf and give_up list. It does not
print the sigma (while it could).
Any improvements are welcome.
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\| |
|
| |\
| | |
| | |
| | | |
Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes
|
| |\ \
| | | |
| | | |
| | | | |
Was PR#368: Add example in dev/doc/changes involving Tacmach.project
|
| |\ \ \
| | | | |
| | | | |
| | | | |
| | | | | |
Was PR#369: Make a note about wit_constr and Constrarg in
dev/doc/changes
|
| |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#371: Update dev/doc/changes with things about mem_named_context
|
|\| | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
| | |_|_|/
| |/| | | |
|
| |/ / / |
|
| |/ / |
|
| |/ |
|
|\| |
|
| |
| |
| |
| | |
It may be worth it, also added a note about file reorganization.
|
| |
| |
| |
| |
| | |
The recommended way to install Coq under windows is anyway to use the
precompiled installer.
|
| | |
|
| | |
|
| | |
|
| | |
|
|\| |
|
| |\ |
|
| | | |
|
| |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This patch converts the `search_*` functions to use an iter-style API.
Consequently, the Search Vernac will produce a message for each search
result, greatly improving roundtrip time as IDEs can effectively display
the results in a streaming way.
It also allows different printers to be used.
I didn't observe a performance difference (as things seem to be
dominated by printing and `Declaremods`).
As a minor tweak, we make search with "Output Name Only" more efficient.
Motivation:
-----------
Currently, the main search API `Search.generic_search` is an effectful,
iteration-based function:
```ocaml
val generic_search : int option -> display_function -> unit
```
This type is imposed by `Declaremods`, which exposes an effectful,
iteration-based API to traverse Coq library objects.
The `Search.search_*` functions try to offer a more functional API by
returning a list of pretty printing commands. They need to build an
internal intermediate list for that purpose.
However, this is a waste of time, as the destination of these lists is
to be flushed out by the printer right away.
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
The word "increment" is more appropriate in this case than "lifting".
The world "lifting", in computer science, usually denotes something else:
https://en.wikipedia.org/wiki/Lambda_lifting
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
8a8caba3).
- Adding cLexer.current_file to the lexer state, i.e. making it a
component of the type "coq_parsable" of lexer state (it was
forgotten in b8ae2de5 and 8a8caba3).
- Inlining save_translator/restore_translator which have now lost most
of their substance.
|
|\| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.
|
| | |
|
| | |
|
|\ \ |
|
| | | |
|
| | | |
|
| | | |
|