| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
Like coqc: detect if the current directory was set by options, if not: add
it with empty logical path.
TODO: check if coq_makefile is still correct wrt to this modification, I
think yes, actually it should end being more correct.
|
|
|
|
|
|
|
|
for reporting it.
A "cut" was not appropriately chained on the second goal but on both
goals, with the chaining on the first goal introducing noise.
|
|
|
|
Syntactic analysis of dependencies when atomizing arguments in destruct
was not dealing properly with primitive projections hiding their
parameters.
|
|
|
|
proofs.
|
|
whd_evar in refresh_universes.
|
|
|
|
inconsistent).
|
|
When refreshing a type variable, always use a rigid universe to force the most
general universe constraint, as in 8.4.
|
|
is buggy in general.
|
|
|
|
Now doing
```coq
Tactic Notation "left" "~" := left.
Tactic Notation "left" "*" := left.
```
will no longer break the `left` tactic in Coq 8.4.
List obtained via
```
grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g'
```
|
|
|
|
|
|
make them rigid to disallow minimization.
|
|
|
|
|
|
its main interest!
|
|
The "master" label used to be reset to the wrong id
|
|
|
|
When a future is fully forced (joined), the fix_exn is dropped,
since joined futures are values (hence they cannot raise exceptions).
When a future for a transparent definition enters the environment
it is joined. If one needs to pick its fix_exn, he should do it
before that.
|
|
(Fix bug #3654)
|
|
involving Futures.
|
|
|
|
universes are declared correctly in the enclosing proofs evar_map's.
|
|
|
|
Without this expansion, camlp4 fails to properly factor a user notation
starting with either "trivial" or "auto".
|
|
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 discharging it is important that constants occur in the libstack
in an order that respects the dependencies among them. This is
impossible to achieve for private constants when they are exported globally
without this (ugly IMO) api.
|
|
|
|
Universe instances for constructors were not always correct, for instance in:
[cons _ list (nil _)] with a polymorphic [list] type, [nil] was receiving an
empty instance.
|
|
- Universes are now represented in the VM by a structured constant containing the
global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
constructor arguments, which has to be prevented.
Was showing up for instance when evaluating [cons _ list (nil _)] with
a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.
Patch written with Benjamin Grégoire.
|
|
Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
|
