| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Should be semantically equivalent.
|
|
Should be semantically equivalent.
|
|
|
|
|
|
|
|
We restrict to those that are actually related to typeclasses, and
perform the following renamings:
Classops --> Coercionops
Class --> ComCoercion
|
|
only-printing notations
Ack-by: cpitclaudel
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: ejgallego
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
- Warn in some places where {x:T} is not assumed to occur (e.g. in
argument of an application, or of a match).
- Warn when an implicit argument occurs several times with the same name.
- Accept local anonymous {_:T} with explicitation possible using name `arg_k`.
We obtain this by using a flag (impl_binder_index) which tells if we
are in a position where implicit arguments matter and, if yes, the
index of the next binder.
|
|
This moves the encoding of "n" as "arg_n" closer to the user interface level.
Note however that Constrintern.build_impl is not able yet to use ExplByPos.
See further commits.
|
|
We renounce to the ad hoc rule preferring a notation w/o delimiter
for a term with coercions stripped over a notation for the
fully-applied terms with coercions not removed.
Instead, we interleave removal of coercions and search for notations:
we prefer a notation for the fully applied term, and, if not, try to
remove one coercion, and try again a notation for the remaining term,
and if not, try to remove the next coercion, etc.
Note: the flatten_application could be removed if prim_token were able
to apply on a prefix of an application node.
|
|
refined version of #8890 which prevents #11033.
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
|
|
We restrict #8890 so that it looks for a notation only for the fully
applied coercion.
|
|
`Fixpoint` with a let binder
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
* map special floats to registered CRef's
* kernel/float64.mli: add {is_infinity, is_neg_infinity} functions
* kernel/float64.ml: Replace string_of_float with a safe pretty-printing function
Namely:
let to_string_raw f = Printf.sprintf "%.17g" f
let to_string f = if is_nan f then "nan" else to_string_raw f
Summary:
* printing a binary64 float in 17 decimal places and parsing it again
will yield the same float, e.g.:
let f1 = 1. +. (0x1p-53 +. 0x1p-105)
let f2 = float_of_string (to_string f1)
f1 = f2
* OCaml's string_of_float gives a sign to nan values which shouldn't be
displayed as all NaNs are considered equal here.
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
|
|
Fixes #9428. (Again.)
This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them.
Corrects a 8.9.1 → 8.10.0 regression.
(cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)
|
|
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
|
|
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
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.
|
|
Fixes #10640
We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.
No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.
Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.
|
|
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.
|
|
We split the function used to retrieve the local context from the one used to
provide the implicit status of each binder. Most of the users only rely on the
former indeed.
|
|
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.
|
|
|
|
|
|
|
|
|
|
Not sure what this was for.
|
|
We can use logical kind for the same purpose, which is mainly
dumpglob, so `goal_object_kind` was never matched against, making this
transformation safe.
|
|
The whole business of cst_kind is fishy tho, it seems to me that it
should be removed from the libobject path.
|
|
We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.
The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.
Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.
IMO this needs more work, but this should be a good start.
|
|
Nobody really knows where this module should belong, it seems. My personal
theory is that it should live in vernac instead, but due to nasty
interactions with abstract-like tactics, we have to put it somewhere below.
|
|
local fix/cofix (#10197)
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
|
