| Age | Commit message (Collapse) | Author |
|---|
|
artificially restricted to a non-empty context).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Because the argument given to refine may mess with the evarmap, the goal being
refined can be solved by side-effect after the term filler is computed. If this
happens, we simply don't perform the refining operation.
|
|
|
|
|
|
It is no longer accepted by Coq's ./configure.
|
|
|
|
|
|
|
|
|
|
|
|
#958
|
|
|
|
|
|
|
|
|
|
The Software Foundations archive has been replaced by three volumes.
|
|
|
|
|
|
For some reason, OPAM was not happy after we reinstalled curl.
|
|
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
|
As explained in BZ#5713 report, the requirement for a non-empty
context is not needed, so we remove it.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
