| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: SkySkimmer
|
|
Tests moved in https://github.com/whonore/Coqtail/pull/134.
|
|
Reviewed-by: anton-trunov
|
|
documentation
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: jfehrle
|
|
recognition.
Reviewed-by: mattam82
|
|
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
exist
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
of artificial dependencies disappearing by reduction
Reviewed-by: ppedrot
|
|
declaring name
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
|
|
|
Alternative to adding this feature to coqbot (coq/bot#14).
|
|
be added
Reviewed-by: CohenCyril
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
|
|
|
|
|
|
We fix it by reducing K-redexes the same in the both places
(make_tuple and minimal_free_rels) which compute the dependencies of a
dependent equality.
|
|
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
|
|
|
|
All except `pair_equal_spec` completely addressed by moving
dependent hypotheses before the colon.
|
|
This is related to coq/coq#6781.
Most issues are with `destruct H` where H is the name of a binder
in the goal; this is addressed by moving dependent assumptions
before the colon. A different option would be adding `intros`
tactics, but this repeats the names of hypotheses (in the type of
the goal and in the proof script).
Additionally, the `destruct H with (Q:=...)` form gets changed to
`destruct (H ...)`, since the binder name `Q` is refreshed.
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
|
|
|
|
We know statically that it is going to be the one provided at the time of
lookup, so we simply fetch it from there.
|
|
|
|
It now silently does nothing rather than erroring with `mv: cannot stat
'output/*.out.real': No such file or directory` if there is no output to
approve, and also correctly handles `output-coqtop` and `output-coqchk`
rather than ignoring these directories.
Fixes #12863
|
|
When calling an Ltac function, add specific locations when
interpreting the function, when interpreting the arguments and when
executating the call (in a TacArg).
|
|
This is important for TacArg arguments, which typically corresponds to
calling an Ltac function.
|
|
|
|
Reviewed-by: jfehrle
|
|
Reviewed-by: mattam82
|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
|
|
The two implementations are essentially the same except for potential
interleaving of let-bindings and pattern-matchings. The only place
the removed function was called probably does not rely on this difference
of behaviour.
|
|
Instead of having to go through the pattern translation, we compute the
pattern directly from the term.
|
|
|
|
test files.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Reviewed-by: mattam82
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
The directory is obsolete since 7461fe4f.
|
|
Reviewed-by: ppedrot
|
|
If we need to print the name of an inlined constant (as in "let name =",
"val name :" or "type name ="), we need its name without inlining nor
qualification.
In particular, we introduce a function pp_global_name to make it
clearer that printing a name at declaration point of a global is only
about printing the basename (formerly, Common.pp_global was correctly
printing the basename without qualification thanks to the
"top_visible_mp ()" test, but OCaml.pp_global was wrongly inlining).
|
|
Fix #7015
|
