| Age | Commit message (Collapse) | Author |
|---|
|
Add headers to a few files which were missing them.
|
|
Check that we don't regress on PR #10762 example
Fix regression discovered by Arthur in PR #10762
Fix script of #10298 which was relying on breaking semantics for `eapply`
Add doc
Add comment in clenvtac
Actually, always mark shelved goals as unresolvable
Update doc to reflect semantics w.r.t. shelved subgoals
|
|
|
|
We remove unused parts of the API, almost all of them belonging to the
legacy engine. This was detected using coverage testing.
The list is provisional and should be subject to change, let's see
what CI says.
|
|
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
|
|
|
|
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
|
|
|
|
|
|
|
|
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
|
|
|
|
|
|
|
|
|
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
|
|
Refine fix for bug #4763, fixing #5149
Tactic [Refine.solve_constraints] and global option
Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.
Fix test-suite files too.
|
|
goal is under focus and which support returning a relevant output.
|
|
|
|
|
