| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
|
|
This is a footgun as it can refresh the name. Callers can still ignore
the generated name by doing `intro_using_then id (fun _ -> tclUNIT())`.
|
|
|
|
|
|
Copy tclWRAPFINALLY to tactics.ml
As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't export
it from Proofview, because it seems somehow not primitive enough. But
we don't export it from Tactics because it is more of a tactical than a
tactic. But we don't export it from Tacticals because all of the
non-New tacticals there operate on `tactic`, not `Proofview.tactic`, and
all of the `New` tacticals that deal with multi-success things are
focussing, i.e., apply their arguments on each goal separately (and it
even says so in the comment on `New`), whereas it's important that
`tclWRAPFINALLY` doesn't introduce extra focussing.
|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
Add headers to a few files which were missing them.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
This is actually dead code, we never observe it.
|
|
|
|
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
|
|
|
|
|
|
|
|
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
|
|
|
|
|
|
This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.
|
|
|
|
|
|
The previous implementation was calling a lot of useless unification
even though the net effect of the tactic was simply to add a binding to
the environment.
Interestingly the base tactic was used in several higher level tactics,
including evar and ssreflect pose.
Part of the fix for #8245.
|
|
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
|
We move the "flag types" to its use place, and mark some arguments
with named parameters better.
|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
In locally nameless mode (proof mode) names in the context *must*
be distinct otherwise the term representation makes no sense.
|
|
We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.
Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
We solve some modularity and type duplication problems by moving types
to a better place. In particular:
- We move tactics types from `Misctypes` to `Tactics` as this is their
proper module an single user [with LTAC].
- We deprecate aliases in `Tacexpr` to such tactic types.
cc: #6512
|
|
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
This is a first step towards some of the solutions proposed in #6008.
|
|
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
|
|
|
|
|
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.
|
|
evars.
This is for consistency with the rest of the language. For instance,
"eremember" and "epose" are supposed to refer to terms occurring in
the goal, hence not leaving evars, hence in general pointless.
Eventually, I guess that "e" should be a modifier (see e.g. the
discussion at #3872), or the difference is removed.
|
|
Also move named arguments to the beginning of the functions. As per
https://github.com/coq/coq/pull/201#discussion_r110928302
|
