| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
|
|
This is a continuation on #6183 and another step towards a more
functional interpretation of commands.
In particular, this should allow us to remove the locality hack.
|
|
These work on precomputed build logs (in this case, from a recent
partial build of fiat-crypto).
They are meant to serve as human-readable sanity checks of output
format.
Separate out the sane bits of template/init.sh from the ones messing
with directory structure (which are fragile and make assumptions about
where the calling script is sourcing it from).
N.B. The test-suite removes all *.log files, so we use *.log.in.
N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile,
because coqc, on Windows, doesn't handle cygwin paths passed via
-coqlib, and `pwd` gives cygwin paths.
N.B. We have .gitattributes to satisfy the linter (as per
https://github.com/coq/coq/pull/6149#issuecomment-346410990)
|
|
Previously, it was reverse-ordering timing diffs.
|
|
|
|
|
|
|
|
Note the problem with `create_evar_defs`.
|
|
With a bit of care we can enable full deprecation warnings again in
this funny file.
|
|
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`.
|
|
The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.
|
|
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
|
global proof.
|
|
As a bonus we remove some trailing whitespace, and implement a couple
of hints suggested in the discussion.
|
|
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
|
|
|
See https://github.com/coq/coq/pull/6197
|
|
|
|
|
|
|
|
This setting is a debug assertion, due to the many flags we still
over-approximate setting the flag to true to all interactive
environments. [So the assert is checked in vo compilation]
Fixes #6152.
|
|
|
|
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.
|
|
|
|
Was broken since 8.6.
|
|
This addresses a limitation found in math-comp seq.v file. See the example in
test suite file success/Notations2.v.
To go further and accept recursive notations with a separator made of
several tokens, and assuming camlp5 unchanged, one would need to
declare an auxiliary entry for this sequence of tokens and use it as
an "atomic" (non-terminal) separator. See PR #6167 for details.
|
|
Replaced by ident_decl in #688.
|
|
|
|
|
|
feature.
|
|
|
|
|
|
|
|
|
|
in make.
|
|
|
|
(clause "where" with implicit arguments)
|
|
unbound rel
|
|
|
|
Fixes #4988.
|
|
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to
put any pattern in binders, prefixed by a quote."] its current
placement as well as the hook don't make a lot of sense.
In particular, they prevent parts of Coq working without linking the
parser.
To this purpose, we need to consolidate the `Constrexpr`
utilities. While we are at it we do so and remove the `Topconstr`
module which is fully redundant with `Constrexpr_ops`.
|
|
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
|
|
We require 4.02.3.
|
|
While we are at it we refactor a few special cases of the helper.
|
|
As of Nov 2017, the standard number of entries is 85, it easily goes
up with some other plugins, so 211 seems like a good compromise.
|
