| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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 more regularity.
|
|
Did some manual merge in tactics/tactics.ml.
|
|
|
|
|
|
Hopefully, it will provide with nicer proof terms, in combination with
the commit printing the type of LetIn when the defined term is a proof.
|
|
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.
|
|
- Had to add a Sigma.to_evar_map
- Had to rework coqdep_common.ml{,i} and coqdep.ml
|
|
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.
|
|
|
|
This is not perfect though, some primitives are unsound, and some
higher-order API should use polymorphic functions so as not to depend
on a given level.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
