| Age | Commit message (Collapse) | Author |
|---|
|
More precisely: The equivalent in #7288 (4dab4fc) to the former call
to ltac_interp_name_env was not done anymore when interpreting
uconstr's.
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
This lets the checker verify that we didn't produce nonsense.
|
|
Opening up a lambda should always lift the substitution attached to it.
|
|
AFAICT there is no reason to use interp_open_constr
I used Evd.from_ctx to keep passing evar maps around but maybe we
should be passing ustates instead?
|
|
|
|
|
|
|
|
|
|
intropattern entry in #10239)
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
#10239).
The bug was introduced in #10239 which seems to have actually remained
half-done: "wit_intropattern" and "wit_simple_intropattern" did not
share the same representation of values (val_tag) but the code was
assuming (especially the code for "fresh") that this was shared.
We fix it by sharing the internal representation (`dyn` field in
Tacarg.make0) as suggested by @ppedrot in the discussion of #10239
(this allows also to simplify Taccoerce.is_intro_pattern).
|
|
This helps extraction by not building sigT which can lower to Prop by
template polymorphism.
Bug #10757 can probably still be triggered by using module functors to
hide that we're using Prop from Program Fixpoint but that's probably
unfixable without fixing extraction vs template polymorphism in
general.
In passing we notice that Program doesn't know how to telescope SProp
arguments, we would need a bunch of variants of sigma types to deal
with it (or use Box?) so let's figure it out some other time.
We also reuse the universe instance to avoid generating a bunch of
short-lived universes in the universe polymorphic case.
|
|
Libraries are now handled like other modules.
|
|
This could be Prop (for compat with usual Coq), Set (for HoTT),
or actually an arbitrary "i".
Take lower bound of universes into account in pretyping/engine
Reinstate proper elaboration of SProp <= l constraints:
replacing is_small with equality with lbound is _not_ semantics preserving!
lbound = Set
Elaborate template polymorphic inductives with lower bound Prop
This will make more constraints explicit
Check univ constraints with Prop as lower bound for template inductives
Restrict template polymorphic universes to those not bounded from below
Fixes #9294
fix suggested by Matthieu
Try second fix suggested by Matthieu
Take care of modifying elaboration for record declarations as well.
Rebase and export functions for debug
Remove exported functions used while debugging
Add a new typing flag "check_template" and option "-no-template-checl"
This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).
Update checker to the new typing flags structure
Switch on the new template_check flag to allow old unsafe behavior in
indTyping.
This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.
Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while
Fix `Template Check` option name and test it
Add `Unset Template Check` to Coq89.v
Cooking of inductives and template-check tests
Cleanup test-suite file for template check / universes(template) flags
cookind tests
Move test of `Unset Template Check` to the failure/ dir, but comment it
for now
Template test-suite test explanation
Overlays for PR 9918
Overlay for paramcoq
Add overlay for fiat_parsers (-no-template-check)
Add overlay for fiat_crypto_legacy
Update fiat-crypto legacy overlay
Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.
Remove overlay that should no longer be necessary
The setting in the compat file should handle it
Remove now-merged fiat-crypto-legacy overlay
Update `Print Assumptions` to reflect the typing flag for template checking
Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic
Fix pretty printing to print global universe levels properly
Fix printing of template polymorphic universes
Fix pretty printing for template polymorphism on no universe
Fix interaction of template check and universes(template) flag
Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe
Indtyping fixes for template polymorphic Props
Allow explicit template polymorphism again
Adapt to new indTyping interface
Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).
Fix check of meaningfullness of template polymorphism in the kernel.
It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.
Comment on identity non-template-polymorphism
Remove incorrect universes(template) attributes from ssr
simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).
Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance
Remove incorrect uses of #[universes(template)] from the stdlib
Extraction of micromega changes due to moving an ind decl out of a section
Remove incorrect uses of #[universes(template)] from plugins
Fix test-suite files, removing incorrect #[universes(template)] attributes
Remove incorrect #[universes(template)] attributes in test-suite
Fix test-suite
Remove overlays as they have been merged upstream.
|
|
|
|
The documentation states:
- Norm means the term is fully normalized and cannot create a redex
when substituted
- Cstr means the term is in head normal form and that it can
create a redex when substituted (i.e. constructor, fix, lambda)
|
|
rewrite
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82
|
|
Fixes #10300 and #10285.
|
|
|
|
This is deemed to be more natural as most of the uses will follow this
structure.
|
|
The previous implementation allowed to dynamically decide whether a section
would be monomorphic or polymorphic at the first definition of a variable
or a constraint. Instead of relying on this delayed decision, we set the
universe polymorphic property directly at the time of the section definition.
|
|
Ack-by: SkySkimmer
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
local fix/cofix (#10197)
Reviewed-by: maximedenes
|
|
Reviewed-by: herbelin
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.
Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.
|
|
|
|
Type's argument
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
|
|
|
|
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
|
|
|
|
|
|
generalization + cleanups
Reviewed-by: herbelin
|
|
The recursive functions and their binders were not pushed in the right
order for implicit arguments.
Additionally, we avoid calling push_name_env both for interpreting the
type of each component of a (co-)fixpoint and for interpreting again the
body of each component of a (co-)fixpoint because it may have
side-effects (in the glob file). So we instead remember the part of
its action on implicit arguments to replay it functionally.
|
|
|
|
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.
The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.
We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.
Fixes #3632 #3890 #4638.
|
|
|
|
|
|
|
|
I don't think there's a reason to treat such variables more severely
than unbound variables. This anomaly is often raised by debug printers
(e.g. when studying complex scenarios using `Set Unification Debug`),
and so makes debugging less convenient.
Fixes #3754, fixes #10026.
|
|
specification
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl
|
|
as assumptions
Ack-by: RalfJung
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
Ack-by: robbertkrebbers
|
|
There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v
* comment the implementations with loop invariants to enable an easy
pen&paper proof of correctness (note to reviewers: the one in
uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
(only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
(cmp is computed at the end of the first loop rather than at the beginning,
potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
new specifiation of div21
* add a test
|
