| Age | Commit message (Collapse) | Author |
|---|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
By default Coq stdlib warnings raise an error, so this is really required.
|
|
|
|
There was also a non truly recursive in the doc.
|
|
|
|
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
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.
|
|
|
|
sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
This removes various compatibility notations.
Closes #8374
This commit was mostly created by running `./dev/tools/update-compat.py
--release`. There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.
The update to CHANGES.md was manual.
|
|
- Improved reification for Micromega (support for #8764)
- Fixes #9268: Do not take universes into account in lia reification
Improve #9291 by threading the evar_map during reification.
Universes are unified.
- Remove (potentially cyclic) dependency over lra for Rle_abs
- Towards a complete simplex-based lia
fixes #9615
Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.
For scalability, nia is currently NOT performing this pre-processing.
- Lia is using the FSet library
manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
to work around a "leaked" hint breaking compatibility of eauto
|
|
(warn if bar is a nonprimitive projection)
|
|
|
|
Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
|
|
All changes done with
```
git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g'
```
As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and
https://github.com/coq/coq/issues/8383#issuecomment-426200497
|
|
|
|
Removing in passing two Local which are no-ops in practice.
|
|
|
|
|
|
|
|
|
|
|
|
Fix new deprecation warnings in the standard library.
|
|
This was decided during the Fall WG (2017).
The aliases that are kept as deprecated are the ones where the difference
is only a prefix becoming a qualified module name.
The intention is to turn the warning for deprecated notations on.
We change the compat version to 8.6 to allow the removal of VOld and V8_5.
|
|
|
|
|
|
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
|
|
|
The statements xelements_bits_lt_1 and xelements_bits_lt_2 had an
unexpected extra dependency due to a name collision with a section
variable.
|
|
The user now has to manually load them, respectively via:
Require Extraction
Require Import FunInd
The "Import" in the case of FunInd is to ensure that the
tactics functional induction and functional inversion are indeed
in scope.
Note that the Recdef.v file is still there as well (it contains
complements used when doing Function with measures), and it also
triggers a load of FunInd.v.
This change is correctly documented in the refman, and the test-suite
has been adapted.
|
|
automatically instead
|
|
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
|
|
|
if_then_else definition does not account for multi success tactics.
tryif_then_else is a primitive tactical with the expected behavior.
|
|
|
|
This way, it's not eaten by a section
|
|
This definition was removed by a4043608f704f026de7eb5167a109ca48e00c221 (This commit adds full universe polymorphism and fast projections to Coq), for reasons I do not know. This means that things like `unfold option_map` work only in 8.5, while `unfold <application of Facts>.option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5.
|
|
There were three versions of injection:
1. "injection term" without "as" clause:
was leaving hypotheses on the goal in reverse order
2. "injection term as ipat", first version:
was introduction hypotheses using ipat in reverse order without
checking that the number of ipat was the size of the injection
(activated with "Unset Injection L2R Pattern Order")
3. "injection term as ipat", second version:
was introduction hypotheses using ipat in left-to-right order
checking that the number of ipat was the size of the injection
and clearing the injecting term by default if an hypothesis
(activated with "Set Injection L2R Pattern Order", default one from 8.5)
There is now:
4. "injection term" without "as" clause, new version:
introducing the components of the injection in the context in
left-to-right order using default intro-patterns "?"
and clearing the injecting term by default if an hypothesis
(activated with "Set Structural Injection")
The new versions 3. and 4. are the "expected" ones in the sense that
they have the following good properties:
- introduction in the context is in the natural left-to-right order
- "injection" behaves the same with and without "as", always
introducing the hypotheses in the goal what corresponds to the
natural expectation as the changes I made in the proof scripts for
adaptation confirm
- clear the "injection" hypothesis when an hypothesis which is the
natural expectation as the changes I made in the proof scripts for
adaptation confirm
The compatibility can be preserved by "Unset Structural Injection" or
by calling "simple injection".
The flag is currently off.
|
|
|
|
Fixes #3379 and part of #3363. Also avoids fragile code propagating required
libraries when closing an interactive module.
Had to fix a few occurrences in std lib.
|
|
|
|
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
|
Printing All cases (bug #3597).
- Fix Ltac matching with primitive projections (bug #3598).
- Spotted a problem with printing of constants with maximally implicit
arguments due to strange "compatibility" interpretation of Arguments [X]
as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
|
|
|
