| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
polymorphic definitions.
- This implementation passes universes in separate arguments and does not
eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
|
|
|
|
After all, let's target 8.6.
|
|
This makes sense probably on Windows too, to be evaluated, maybe .exe
suffix should be added.
|
|
Since the functions of this plugin exit by raising exceptions, globing
was never restarted. This prevented coqdoc from generating a proper
output whenever some feature of this plugin was used. There does not seem
to be any parsing of dynamic expressions, so pausing globing does not make
much sense in the first place.
|
|
structure.
|
|
paths for ocaml* executables in the generated config/Makefile.
Hoping I'm not doing something wrong. E.g., I don't see why it would
not be ok for windows or macosx too, since e.g. camlp5o was already
with a full path.
|
|
- usage ill-formed for -native-compiler
- compatibility with the configure of 8.4 (-force-caml-version),
though e.g. its force-ocaml-version alias is no longer supported
(but at the same time not documented either, so...)
|
|
are redhibitory.
|
|
|
|
|
|
|
|
As shown by the code snippets in these bug reports, I've been too
hasty in considering these situations as anomalies in commit 466c4cb
(at least the one at the last line of consistency_checks). So let's turn
these anomalies back to regular user errors, as they were before this commit.
|
|
|
|
When F is a Functor, doing an 'Include F' triggers the 'Include Self'
mechanism: the current context is used as an pseudo-argument to F.
This may fail with a subtype error if the current context isn't adequate.
|
|
For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc461).
|
|
by the type to prove (was introduced in 35846ec22, r15978, Nov 2012).
Not only it does not work when exact is called via a Ltac definition,
but, also, it does not scale easily to refine which is a TACTIC
EXTEND.
Ideally, one may then want to propagate scope interpretations through
ltac variables, as well as supporting refine...
See #4034 for a discussion.
|
|
|
|
Was introduced in b06d3badb (15 Jul 2015).
|
|
|
|
|
|
The detection of new hypothesis was bugged.
Now infoH behaves like "Show Intros": it performs tac, grab
information on hypothesis names but let the state unchanged.
FTR: infoH is fundamentally unable to be correct in presence of
tactics that delete hypothesis and reuse there names. Like destruct or
induction. Fortunately destruct and induction now come with a variant
asking that the hypothesis is not deleted. To guess for the right
as-close for [induction H], do [infoH induction !H]. This will not
create the same names as induction would have by itself but at least
there will be the right number of hypothesis.
|
|
Update the evar_source of the solution evar in evar/evar problems to
propagate the information that it does not necessarily have to be solved
in Program mode.
|
|
|
|
|
|
|
|
presence of dependent types with only superficial dependency).
See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372.
|
|
|
|
|
|
|
|
|
|
variables of the context of an evar in debugging mode.
|
|
starting a sentence with a symbolic expression.
|
|
of the return clause and of the branches (what assumed that the
implementation preserves the invariant that the return predicate and
the branches are in canonical [fun Δ => t] form, with Δ possibly
containing let-ins).
|
|
dealing with "match".
Contrastingly, "fix" is considered not to count let-ins for finding
the recursive argument (which is ok because the last argument is
necessarily a lambda).
|
|
to compensate decompose_lam_n_assum which does not count let-ins.
Any idea on a uniform and clear naming scheme for this kind of
decomposition functions?
|
|
This was a trivial overlook.
|
|
|
|
|
|
Was introduced by seemingly unrelated commit
fd62149f9bf40b3f309ebbfd7497ef7c185436d5.
The currently policy is to avoid exposing global references in the kernel
interface when easily doable.
|
|
|
|
Using the same hack as in the kernel: VM conversion is a reference to
a function, updated when modules using C code are actually linked.
This hack should one day go away, but always linking C code may produce some
other trouble (with the OCaml debugger for instance), so better be safe
for now.
|
|
|
|
|
|
|
|
Previously, the kernel was silently switching back to the standard conversion.
|
|
|
|
This commit has no impact, since l2r is always false in practice due to
the definition of default_conv.
|
