| Age | Commit message (Collapse) | Author |
|---|
|
Now [unshelve tac1; tac2] is parsed as [(unshelve tac1); tac2].
|
|
This tactical is inspired by discussions on the Coq-club list. For now
it is still undocumented, and there is room left for design issues.
|
|
|
|
on applications of inverse (flip) on a crelation.
This was poluting universe constraints of lemmas using generalized
rewriting in Type.
|
|
|
|
|
|
|
|
|
|
The issue was due to the fact that unfold hints are given a priority of 4
by default. As eauto was now using hint priority rather than the number of
goals produced to order the application of hints, unfold were almost always
used too late. We fixed this by manually giving them a priority of 1 in the
eauto tactic.
Also fixed the relative order of proof depth w.r.t. hint priority. It should not
be observable except for breadth-first search, which is seldom used.
|
|
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
|
|
|
|
Everywhere we know that the universes of the left argument are an
extension of the right argument, we do not have to merge universes.
|
|
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
|
|
|
|
|
|
|
|
|
|
For pose/set/clearbody, I think it is clear that we want to preserve
the name and this commit do it.
For revert, I first did not preserve the name, then considered in
2ba2ca96be88 that it was better to preserve it.
For intro, like for revert actually, I did not preserve the name,
based on the idea that the type was changing (*). For instance if we have
?f:nat->nat, do we really want to keep the name f in ?f:nat after an
intro.
For revert, I changed my mind based on the idea that if we had a
better control of the name if we keep the name that if the system
invents a new one based on the type. I think this is more reasonable
than (*), so this commit preserves the name for intro.
For generalize, it is still not done because of generalize being in
the old proof engine.
|
|
Syntactic analysis of dependencies when atomizing arguments in destruct
was not dealing properly with primitive projections hiding their
parameters.
|
|
inconsistent).
|
|
is buggy in general.
|
|
|
|
|
|
It is too bad that OCaml does not warn when catching an exception over a
closure rather than inside it.
|
|
presence of hints modifying the context and of a "using" clause.
Incidentally opening Hints by default in debugger.
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
|
|
|
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.
|
|
|
|
presence of dependent types with only superficial dependency).
See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372.
|
|
|
|
|
|
Instead of brutally merging the whole evarmap coming from the clenv,
we remember the context associated to the hint and we only merge that tiny
part of constraints. We need to be careful for polymorphic hints though,
as we have to refresh them beforehand.
|
|
|
|
|
|
|
|
|
|
Collecting the bound variables is now done on the glob_constr, before
interpretation, so that only variables given explicitly by the user
are used for binding bound variables.
|
|
their polymorphic status _and_ locality.
|
|
It was wrong, the context was readded needlessly to the local evar_map context.
|
|
|
|
According to their polymorphic/non-polymorphic status, which
imply that universe variables introduced with it are assumed
to be >= or > Set respectively in the following definitions.
|
|
|
|
|
|
|
|
with Enrico.
|
|
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
|
|
We purge the environment given to the morphism searcher from all dependencies
on the considered variable. I hope it is not too costly.
|
