| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
Was PR#301: Update .gitignore with new names for psatz caches.
|
|
Was PR#326: Extend documentation of auto
|
|
+ a few improvements on 5f1dd4c40 (lexing of { and }).
|
|
|
|
|
|
|
|
|
|
New fix. A bit less consistent with the spirit of this Makefile as we
list prerequisite files explicitly, but avoid to redo subsystems at
each call to "make" as with previous fix.
Other solutions from experts are welcome.
|
|
|
|
This assertion checked that two arguments in the same position were equal,
but in fact, since one might have already been reduced, they are only
convertible (which is too costly to check in an assertion).
|
|
When inserting a character in an already processed buffer, a message is
sent to Coq so that the proof is backtracked and the character is
inserted. If a second character is inserted while Coq is still busy with
the first message, the action is canceled, but the signal is no longer
dropped so that the second character is properly inserted.
|
|
|
|
|
|
|
|
|
|
|
|
This is useful for debugging purposes.
|
|
This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a.
A good fix requires to review a bit the design of unification constraint
postponement, which we do in 8.6. We leave things as they are in 8.5 for
compatibility.
|
|
|
|
This makes [refine] typecheck the term only once (instead of twice),
(Qed excluded of course). Fix test-suite file for output of constraints
accordingly.
|
|
|
|
Was PR#328: Change the order of arguments of fig2dev.
|
|
Was PR#233: [search] Search result streaming
|
|
|
|
If an existing evar was cleared in pretyping (typically while
processing "ltac:"), it created an evar considered as new. Updating
them instead along the "cleared" flag.
If correct, I suspect similar treatment should be done for refining
along "change", "rename" and "move".
|
|
|
|
The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.
The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.
Adapt test-suite files accordingly.
|
|
|
|
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
|
|
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.
|
|
|
|
This function does the same thing as "Names.Id.List.mem" so:
- I deleted the "Namegen.to_avoid" function and
- replaced all calls of "Namegen.to_avoid" to calls of "Names.Id.List.mem"
|
|
|
|
It now prints evars with candidates as well if there are any.
|
|
These variants are from 8.3 but were never documented except in CHANGES.
|
|
|
|
When trying different possible return predicates, returns the error
given by the first try, assuming this is the most interesting one.
|
|
|
|
|
|
|
|
The doc of auto hints now mention again that sometimes a hint
will be used with simple apply and sometimes it will be used
with exact.
It does not try to be fully precise in that we don't
necessarily want to document the behaviors of auto that
we might like to change.
See also the discussion on commit 9227d6e.
|
|
|
|
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
|
|
For some reason "grammar/grammar.cma" was declares only an "order-only" dependency for "*.ml" files generated from "*.ml4".
I this that this is a problem because when we change "grammar/*.mlp" files, even tough "grammar/grammar.cma" is regenerated,
the actual "*.ml" files (defined by "*.ml4" as well as "grammar/grammar.cma") are not regenerated.
|
|
For some reason, with my version of transfig (which seems to be the latest),
the order of arguments of the fig2dev command matters: -L png must come
before -m 2. I suppose that this fix shouldn't break things for others.
|
