| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Extraction Language command
|
|
|
|
We remove a few old-style normalization and try to use the newer APIs,
however, it is hard to say whether the right magic is being used.
|
|
|
|
repository. Also removing FAQ-related build rules.
|
|
|
|
|
|
|
|
|
|
This is useful as it allows to reflect program_mode behavior as an attribute.
|
|
Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.
We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.
This patch depends on #6413.
|
|
`ssrnat` is mentioned, but it is not distributed with Coq.
|
|
|
|
Enable builds on Windows by removing Windows-style endings where it impacts make.
The fix in Makefile.build is a band-aid fix; maximedenes said he would remove the dependency on sed and awk here.
|
|
Let definitions have the same behaviour if they are ended with a Qed or a
Defined command, i.e. they are treated as if they were transparent. Indeed,
it doesn't make sense for them to be opaque as they are going to be expanded
away at the end of the section.
For an unknown reason, handling of side-effects in Let definitions considers
them as if they were opaque, i.e. the effects are inlined in the definition.
This discrepancy has bad consequences in the kernel, where one is forced to
juggle with universe constraints generated by polymorphic Let definitions.
As a first phase of cleaning, we simply enforce by typing that Let definitions
should be purified before reaching the kernel.
This has the intended side-effect to make side-effects persistent in Let
definitions, as if they were indeed truly transparent.
|
|
- In ocamlfind-based byte builds, link the VM statically as in native
builds. This is the best way to get reliable, path-independent
self-contained executables.
- In `make install`, install the `.cmx` files for plugins too. To
statically link Coq plugins in native mode, both the `.cmx` and `.o`
files must be present.
|
|
This is a very useful feature for IDEs, as they can queue commands and display options in a single request. Change is backwards-compatible.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
|
|
Universe instances were lost during constructions of the canonical instance.
|
|
Travis has moved on to macOS 10.12 but this makes the package
incompatible with earlier versions.
This fix should restore the compatibility with OS X 10.11.
|
|
As per request at https://github.com/coq/coq/pull/6406#pullrequestreview-83503902
|
|
This closes #5082 and closes #5778, but makes #6404 apply to `abstract`
as well as `transparent_abstract`. This is unfortunate, but I think it
is worth it to get `abstract` in the profile (and therefore not
misassign the time spent sending the subproof to the kernel). Another
alternative would have been to add a dedicated entry to `ltac_call_kind`
for `TacAbstract`, but I think it's better to just deal with #6404 all
at once.
The "better" solution here would have been to move `abstract` out of the
Ltac syntax tree and define it via `TACTIC EXTEND` like
`transparent_abstract`. However, the STM relies on its ability to
recognize `abstract` and `solve [ abstract ... ]` syntactically so that
it can handle `par: abstract`.
Note that had to add locations to `TacAbstract` nodes, as I could not
figure out how to call `push_trace` otherwise.
|
|
|
|
|
|
|
|
I'm not sure if they belong in profile_ltac, or in extratactics, or,
perhaps, in a separate plugin. But I'd find it very useful to have a
version of `time` that works on constr evaluation, which is what this
commit provides.
I'm not sure that I've picked good naming conventions for the tactics,
either.
|
|
|
|
This is useful for tactics that run a bunch of tests and need to display
the profile for each of them.
|
|
|
|
(fix #6106)
|
|
|
|
|
|
|
|
same right-hand side.
|
|
arguments.
|
|
|
|
|
|
|
|
This enforces the intended meaning of the corresponding functions
(prod_appvect*/prod_applist*).
|
|
Adding a "let-in"-sensitive function hnf_prod_applist_assum to
instantiate parameters and using it for printing.
Thanks to PMP for reporting.
|
|
Was introduced in e8c47b65.
|
|
|
|
|
