| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Adding also tclSETSHELF/tclGETSHELF by consistency with
tclSETGOALS/tclGETGOALS.
However, I feel that this is too low-level to be exported as a
"tcl". Doesn't a "tcl" mean that it is supposed to be used by common
tactics? But is it reasonable that a common tactic can change and
modify comb and shelf without passing by a level which e.g. checks
that no goal is lost in the process.
So, I would rather be in favor of removing tclSETGOALS/tclGETGOALS
which are anyway aliases for Comb.get/Comb.set.
Conversely, what is the right expected level of abstraction for
proofview.ml?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
The type discipline of the tactic monad does not distinguish between
mono-goal and multi-goal tactics. Unfortunately enter_one "asserts
false" if called on 0 or > 1 goals. The __LOC__:string argument can
be used to make the error message more helpful (since the backtrace is
pointless inside the monad).
The intended usage is "Goal.enter_one ~__LOC__ (fun gl -> ..".
The __LOC__ variable is filled in by the OCaml compiler with the current
file name and line number.
|
|
|
|
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
|
|
|
It is actually polynomial with a big exponent, probably quartic. This was due
to the Proofview.unifiable algorithm that kept recomputing the free evars of
an evar info. We share the computation instead.
This does not make the contrived example compile in a reasonable amount of time,
but it does make smaller instances compile way quicker than before. Indeed, the
example is essentially quadratic in size as all evars refer to the previously
defined ones in their signature.
|
|
The function Proofview.undefined was collecting twice the evars that
had advanced. Consequently, the functions Proofview.unshelve and
Proofview.with_shelf were possibly doing the same.
|
|
|
|
the monad.
|
|
|
|
Pointed out by PMP.
|
|
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 a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).
Incidentally updating output of Show output test (evar numbers shifted).
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
|
|
Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
|
|
Now it is a private field, locations are optional.
|
|
|
|
|
|
|
|
This is now useless as this returns evar-constrs, so that all functions acting
on them should be insensitive to evar-normalization.
|
|
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
|
|
|
|
|
|
|
|
|
|
|
Was PR#350: tclDISPATCH: more informative error message
|
|
|
|
"expected _n_ tactics" -> "exected _n_ tactics, was given _k_".
Also affect other similar tacticals from `Proofview`.
I used that for debugging once, I thought I might as well propose it for
mergeing.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
