| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
When printing evar constraints, we ensure that every variable from the
rel context has a name.
|
| | |
|
| | |
|
| |\
| |
| |
| | |
Was PR#263: Fast lookup in named contexts
|
| | |
| |
| |
| | |
goal is under focus and which support returning a relevant output.
|
| |/ |
|
| |
|
|
|
| |
Essentially, we do not reconstruct the named_context_val when the rel_context
is empty.
|
| |
|
|
|
| |
Before computing the whd_evar-form of the arguments of an evar, we first
check that it is indeed defined.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
|
| | |
|
| |\
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We used to recompute all fresh named contexts for evars before this patch in
the push_rel_context_to_named_context function. This was incurring a linear
penalty and a memory explosion due to the reallocation of many arrays. Now, we
rather remember the context between evar creations by sharing it in the pretyping
environment.
This can be considered as a fix for bug #4964 even though we might do better.
|
| | | |
|
| | |
| |
| |
| | |
This saves a quadratic allocation by replacing arrays with maps.
|
| | |
| |
| |
| |
| | |
In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
We remove in particular a dubious use of an environment in fresh name
generation. The code was using the wrong environment in a function only
depending on the rel context which was resetted most of the time. This
might change the generated names in extremely rare occurences.
|
| |/ |
|
| | |
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
|
| |
|
|
|
| |
For better error messages. The API change is
backwards compatible, using a new optional argument.
|
| |
|
|
| |
Take advantage that the provided term is always a variable in Equality.is_eq_x.
|
| |
|
|
| |
We do not allocate a closure in the main loop, and do so only when needed.
|
| |
|
|
|
| |
We do not check for presence of a variable in a global definition when we know
that this variable was not present in the section.
|
| |
|
|
|
|
|
|
|
| |
We do not recompute shortest name identifier for global references that were
already traversed. Furthermore, we share the computation of identifiers
between invokations of the name generating function.
This drastically speeds up detyping for huge goals, further mitigating the
shortcomings of the fix for bug #4777.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
unshelve_goals is used to correctly register dependent
subgoals that have to be solved. Resolution may fail to
do so using hints, so we have to put them back as goals
in that case. The shelf is a good interface for doing that.
unifiable can be used outside proofview to detect dependencies
between goals. This might be better in another module.
|
| |
|
|
| |
Fix typo in proofview
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
This is the "error resiliency" mode for STM
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |/
|/|
| |
| |
| | |
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
| | | |
|
| |/ |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Guillaume Melquiond
Pierre Letouzey
Matthieu Sozeau
Matthieu Sozeau
Enrico Tassi
Cyprien Mangin
Emilio Jesus Gallego Arias