| Age | Commit message (Collapse) | Author |
|---|
|
relation
Reviewed-by: gares
|
|
|
|
(namely, [RewriteRelation]s beyond Equivalence ones)
Thanks to @CohenCyril for suggesting this enhancement
|
|
* Preserve the same behavior/interface but merge the two Module Types
(UNDER_EQ and) UNDER_REL.
* Remove the "Reflexive" argument in Under_rel.Under_rel
* Update plugin code (ssrfwd.ml) & Factor-out the main step
* Update the Hint (viz. apply over_rel_done => apply: over_rel_done)
* All the tests still pass!
Credits to @CohenCyril for suggesting this enhancement
|
|
|
|
try/with->assert false
as suggested by @gares (the Not_found exc may be catched by coq/ssr otherwise).
|
|
|
|
E.g., if one wish to instantiate these evars manually, in another way
than with reflexivity.
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: gares
|
|
Matthieu Sozeau explained how to fix this.
|
|
As documented in the feedback API.
|
|
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.
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
|
|
|
involving &
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Ack-by: ggonthier
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: vbgl
|
|
Changes:
* Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive];
* Add ssrsetoid.v that links
[ssrclasses.Reflexive] and [RelationClasses.Reflexive];
* Add [Require Coq.ssr.ssrsetoid] in Setoid.v;
* Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that
ports some non-exported material from rewrite.ml;
* Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin;
* Update doc and tests as well.
Summary:
* We can now use the under tactic in two flavors:
- with the [eq] or [iff] relations: [Require Import ssreflect.]
- or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.]
(while [ssreflect] does not require [RelationClasses] nor [Setoid],
and conversely [Setoid] does not require [ssreflect]).
* The file ssrsetoid.v could be skipped when porting under to stdlib2.
|
|
* Add an extra test with an Equivalence.
* Update the doc accordingly.
|
|
|
|
|
|
|
|
We register the ML tactics by hand using the low-level API.
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
Type's argument
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
Reviewed-by: gares
|
|
Ack-by: andreaslyn
Reviewed-by: gares
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
|
|
We consistently use:
- UUnknown: to mean a rigid anonymous universe
(written Type in instances and Type as a sort)
[was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
(written _ in instances and Type@{_} as a sort)
[was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
(written id or qualid in instances and Type@{id} or Type@{qualid} or more
generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)
There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.
There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Using pstate makes no sense for printing global stuff
|
|
|
|
|
|
|
|
This impacts a lot of code, apparently in the good, removing several
conversions back and forth constr.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
** Changed definition of `simpl_rel` to `T -> `simpl_pred T`, so that
`inE` will now expand `a \in r b`, when `r := [rel x y | R]` to `R{b/x,
a/y}`, as the expanding coercion is now only inserted in the _last_
application.
The old definition made it possible to have a `simpl_rel >-> rel`
coercion that does not block expansion, but this can now be achieved
more economically with the `Arguments … /.` annotation.
** Deleted the `[rel of P]` notation which is no longer needed with
the new `simpl_rel` definition, and was broken anyway.
** Added `relpre f R` definition of functional preimage of a notation.
** `comp` and `idfun` are now proper definitions, using the `Arguments
… /.` annotation to specify simplification on application.
** Added `{pred T}` syntax for the alias of `pred T` in the `pred_sort`
coercion class; deleted the `pred_class` alias: one should either
use `pred_sort` in `Coercion` declarations, or `{pred T}` in type casts.
Used `{pred T}` as appropriate in localised predicate (`{in …, …}`) theory.
Extended and corrected `pred` coercion internal documentation.
** Simplified the `predType` structure by removing the redundant
explicit `mem_pred` subfield, and replacing it with an interlocked
projection; deleted `mkPredType`, now replaced by `PredType`.
** Added (and extensively documented) a `nonPropType` interface
matching types that do _not_ have sort `Prop`, and used it to remove
the non-standard maximal implicits annotation on `Some_inj` introduced
in #6911 by @anton-trumov; included `test-suite` entry for `nonPropType`.
** Documented the design of the four structures used to control the
matching of `inE` and related predicate rewriting lemmas; added `test-suite`
entry covering the `pred` rewriting control idioms.
** Used `only printing` annotations to get rid of token concatenation
hacks.
** Fixed boolean and general `if b return t then …` notation so that
`b` is bound in `t`. This is a minor source of incompatibility for
misuses of this syntax when `b` is _not_ bound in `t`, and `(if b then
…) : t` should have been used instead.
** Reserved all `ssreflect`, `ssrfun` and `ssrbool` notation at the top
of the file, adding some printing boxes, and removing some spurious
`[pred .. => ..]` reserved notation.
** Fixed parsing precedence and format of `<hidden n>` notation, and
declared and put it in an explicit `ssr_scope`.
** Used module-and-functor idiom to ensure that the `simpl_pred T >-
pred T` _and_ `simpl_pred T >-> {pred T}` coercions are realised by the
_same_ Gallina constant.
** Updated `CREDITS`.
The policy implied by this PR: that `{pred T}` should systematically
be used as the generic collective predicate type, was implemented in MathComp
math-comp/math-comp#237. As a result `simpl_pred >-> pred_sort` coercions
became more frequent, as it turned out they were not, as incorrectly stated
in `ssrbool` internal comments, impossible: while the `simplPredType`
canonical instance does solve all `simpl_pred T =~= pred_sort ?pT`
instances, it does _not_ solve `simpl_pred T =~= {pred T}`, and so the
coercion will be used in that case. However it appeared that having two
different coercion constants confused the SSReflect keyed matching
heuristic, hence the fix introduced here. This has entailed some
rearrangement of `ssrbool`: the large `Predicates` section had to be
broken up as the module-functor idiom for aliasing coercions cannot be
used inside a section.
|
