| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
Fixes #12845 (coqchk reports names from inner modules of opaque modules
as axioms)
I don't fully understand the code here, so I can't speak as to its
correctness, but it should be simple enough that reviewers can
understand what it's doing and whether or not it's correct.
This is useful for me in making progress towards
https://github.com/mit-plv/fiat-crypto/issues/736
|
|
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).
|
|
We use an indirection, producing the sorted list of subdirectories of
plugins/, so that dune can recognize it hasn't changed and doesn't
rerun configure. Since configure regenerates a timestamp this avoids
recompiling the stdlib.
Fix #12750.
|
|
Fix #7015
|
|
|
|
|
|
OUnit package name is changed from "oUnit" to "ounit2":
https://github.com/gildor478/ounit#user-content-transition-to-ounit2
This change follows it and fixes
a failure, `ocamlfind: Package oUnit not found`,
at `make test-suite` and `dune build`.
|
|
The update of a loc needs sometimes to override (when calling an Ltac
function), and otherwise to keep the existing loc (assumed to be
fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests).
Moreover, when overriding, this was going to a tclOR backtracking
point which was setting the loc to a completely disjoint part of the
code having caused the error (see #12773). We replace the tclOR by a
tclORELSE.
|
|
|
|
|
|
|
|
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
construct
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: jfehrle
|
|
As suggested by Laurent Thery to Chris Dams on Coq-Club.
(And fix the documented syntax in the manual.)
|
|
purely applicative stacks
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Due to the way transparency is handled in hint databases, every time it is
changed, all dnets are recomputed from scratch. This is very expensive, and
a bench showed that it was sometimes contributing significantly to the whole
compilation time of hint-heavy libraries. This patch makes this computation
lazy, so that the dnet is computed only the first time a hint lookup is
performed.
The implementation is functionally equivalent to wrapping the sentry_bnet
field in a Lazy.t, but because dnets are stored in the summary and thus
marshalled, I had to manually perform a defunctionalization.
A (maybe cleaner?) alternative would be to track the set of constants a
hint depend on, in order to only refresh those touched by the change of
transparency. Yet, this would be a much more invasive change.
|
|
Reviewed-by: gares
|
