| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
and disable hashconsing of substituted instances which had a huge performance
penalty in general. They are hashconsed when put in the environment only now.
|
|
|
|
|
|
|
|
|
|
|
|
any prefix of the given qualid.
|
|
The new Term version has essentially the same behaviour as the old "Locate",
while the new raw searches for all types of objects. Also code merging with
the "Locate Ltac".
Fixes bug #3380.
|
|
command.
|
|
|
|
|
|
|
|
unification, speeding it up considerably
Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410
|
|
which
results in strange changes in user provided terms.
|
|
new files (WeakFan.v and WKL.v).
|
|
|
|
|
|
|
|
|
|
given to the obligation making function.
- Fix handling of universe context when solve_by_tac is used.
|
|
Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem
after all.
|
|
|
|
|
|
|
|
|
|
|
|
This bug was hacked around in ssreflect, but with the new idea
that parsing and interpretation are done in distinct phases the
work around could not be implemented anymore.
|
|
|
|
|
|
backtracks, print time spent in each of successive calls.
|
|
|
|
more than one constructor.
|
|
|
|
|
|
This is useful if a UI does not support that
|
|
|
|
|
|
LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
|
|
|
|
|
|
|
|
|
|
a primitive projection impossible.
|
|
|
|
|
|
These are now sufficient to implement PIDE
|
