| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |
|
| | |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| |
| | |
We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
|
| | |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| | |
is buggy in general.
|
| | |
| |
| |
| | |
its main interest!
|
| |\| |
|
| | |
| |
| |
| | |
universes are declared correctly in the enclosing proofs evar_map's.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Do not normalize the type of a proof according to the final universes
when keep_body_ucst_separate is true, otherwise the type might not be
retypable in the initial context...
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
Goal displaying during Debugging ltac is a notice message now. Other
messages are debug messages. This does not change anything in coqide
or coqtop, but allows proofgeneral to dispatch them in the right
buffers (pg had to be fixed too).
|
| |\| |
|
| |\ \ |
|
| | | | |
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| | |
- When there are side effects which might enrich the initial universes
of a proof, keep the initial and refined universe contexts apart like
for delayed proofs, ensuring universes are declared before they are
used in the right order.
- Fix undefined levels in proof statements so that they can't be lowered
to Set by a subsequent, delayed proof.
|
| | |
| |
| |
| |
| |
| | |
This fixes a bug in proofgeneral. PG will now diplay this message
eagerly. Otherwise since they appear before the goal, they are
considered outdated and not displayed.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Enrico Tassi
Pierre Courtieu
Maxime Dénès
Matthieu Sozeau