| Commit message (Collapse) | Author | Age |
... | |
|
|
|
| |
variant of it, accepting an additional integer.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The call to the native compiler can fail due to the sheer amounts of -I
options passed to it. Indeed, it is easy to get the command line to exceed
512KB, thus causing various operating systems to reject it. This commit
avoids the issue by only passing the -I options that matter for the
currently compiled code.
Note that, in the worst case, this commit is still not sufficient on
Windows (32KB max), but this worst case should be rather uncommon and thus
can be ignored for now.
For the record, the command-line size mandated by Posix is 4KB.
|
| |
|
| |
|
| |
|
|
|
|
| |
parsing rule.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
"foobar" constr(x1) ... constr(xn)
are now defined as pure Ltac definitions, and do not add grammar
nor printing rules. This partially relies on a hack consisting
in retrieving the arguments in the tactic environment rather than
as directly passed to the TacExtend node.
|
|
|
|
|
|
|
|
| |
We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.
Some tactics from the AST were also moved away and made using this
mechanism.
|
|
|
|
| |
This reverts commit f3b3b6e4d01080da4f0ce37a06553769e9588d0e.
|
|
|
|
|
|
|
|
|
|
|
|
| |
Example:
Inductive Pnat : Prop := O | S : Pnat -> Pnat.
Variable m n : Pnat.
Goal S (S O) = S O -> False.
intros H; injection H.
now deduces S O = O instead of failing with an error message.
|
| |
|
|
|
|
| |
Use Set Injection On Proof to enable the new behavior.
|
| |
|
| |
|
| |
|
|
|
|
| |
This reverts commit c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2.
|
|
|
|
|
|
| |
the merge).
Obligations are not necessarily opaque.
|
| |
|
| |
|
| |
|
|
|
|
| |
"coretactics.ml4" file.
|
|
|
|
| |
them.
|
|
|
|
|
| |
not create grammar and printing rules anymore, they define Ltac entries
in the module that declares them instead.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
substitutive.
|
| |
|
|
|
|
|
|
|
|
| |
This should be now linear instead of the cubic Bellman-Ford algorithm.
The new algorithm assumes that the universe graph is a DAG if we remove
the {Le, Eq}-cycles, which is the case when the graph is consistent.
Luckily we only use the sorting algorithm on such consistent graphs,
in the Print Sorted Universes command.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
corresponding Declare ML Module command. This changes essentially two
things:
1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.
2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.
|
| |
|
|
|
|
| |
dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro.
|
|
|
|
|
| |
caching time, i.e. when the Declare ML Module command is evaluated. This can
be used by both static and dynamic plugins.
|
| |
|
|
|
|
| |
and the lookup operation proved to be costly when dealing with big libraries.
|
|
|
|
| |
instead of lists to test if a library has already been encountered.
|
|
|
|
|
|
|
|
| |
The contract is that a file in bugs/opened should not raise errors if
the bug is still open.
Some of them fail for different reasons than they used to; I'm not sure
what to do about these.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
hese regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.
These are the tests that trunk currently fails.
I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.
|
| |
|
| |
|
| |
|
|
|
|
| |
fixing two opened bugs from HoTT/coq.
|
|\
| |
| |
| | |
into JasonGross-working-polyproj-tests
|
| |
| |
| |
| |
| | |
abstraction has the right type. Fixes bug# 3306.
Add test-suite files for bugs 3305 and 3306.
|