| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |/ / / / /
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6.
This behavior of refine has changed three times in recent years, so
let's take the time to make up our mind and wait for a major release.
Btw, onhyps=None is not a sane way to express that a tactic should be
applied to all hypotheses.
|
| | |\ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#334: Fix bug 5031 : should not be an anomaly
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
not an anomaly
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | |\ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Was PR#233: Fix a bug in error printing of unif constraints
|
| | | | |\ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Was PR#329: Fix #5127 Memory corruption with the VM
|
| |\| | | | | | | | | |
|
| | |\ \ \ \ \ \ \ \ \
| | | |/ / / / / / /
| | |/| | | | | | | |
|
| | | | | | | | | | | |
|
| | | | | | | | | | | |
|
| | |\ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Was PR#301: Update .gitignore with new names for psatz caches.
|
| | | | |\ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Was PR#326: Extend documentation of auto
|
| | | | | | | | | | | | | |
|
| | | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
The bytecode interpreter ensures that the stack space available at some
points is above a static threshold. However, arbitrary large stack space
can be needed between two check points, leading to segmentation faults
in some cases.
We track the use of stack space at compilation time and add
an instruction to ensure greater stack capacity when required. This is
inspired from OCaml's PR#339 and PR#7168.
Patch written with Benjamin Grégoire.
|
| | | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
+ 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.
|
| | | | | | | | | | | |
|
| | | | | | | | | | | |
|
| | | | |_|/ / / / /
| | |/| | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Conversion problems are in a de Bruijn environment that may
include references to unbound rels (because of the way evars
are created), we patch the env to named all de Bruijn variables
so that error printing does not raise an anomaly. Also fix a minor
printing bug in unsatisfiable constraints error reporting.
HoTT_coq_117.v tests all of this.
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| | |\| | | | | | | |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
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.
|
| | | |_|_|_|_|_|/
| |/| | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.
|
| | |\ \ \ \ \ \ \ |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
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.
|
Maxime Dénès
Yves Bertot
Pierre-Marie Pédrot
Hugo Herbelin
Enrico Tassi
Jason Gross
Guillaume Melquiond
Matthieu Sozeau
Matthieu Sozeau
Emilio Jesus Gallego Arias
Matej Kosik
Théo Zimmermann