| Age | Commit message (Collapse) | Author |
|---|
|
Prevent errors when under annotating binders.
|
|
For nonsquashed:
Either
- 0 constructors
- primitive record
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
|
|
record
Reviewed-by: ejgallego
|
|
This is intended to be separate from handling of implicit binders.
The remaining uses of declare_manual_implicits satisfy a lot of
assertions, giving the possibility of simplifying the interface in the
future.
Two disabled warnings are added for things that currently pass silently.
Currently only Mtac passes non-maximal implicits to
declare_manual_implicits with the force-usage flag set. When implicit
arguments don't have to be named, should move Mtac over to
set_implicits.
|
|
|
|
I think the usage looks cleaner this way.
|
|
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
records
Reviewed-by: ppedrot
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
Ack-by: SkySkimmer
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Fix #8076.
|
|
This makes it print the warning before the definition message, so if
we run with +non-primitive-record we don't see
"""
defined foo
error could not define foo
"""
|
|
This simplifies reasoning about the kernel code.
We still auto downgrade squashed Prop records as the code path to
avoid an error is more involved. Alternatively we could produce an
error forcing people to Unset Primitive Projections if they want a
squashed record.
|
|
The warning can be avoided with the attributes, (or just disable the
warning itself I guess).
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
write_function
|
|
|
|
|
|
(same for solve_remaining_evars)
This is the standard way to use these functions, with 1 exception in
Unification.
|
|
|
|
For now this data is not stored, but the code checks that indeed the number
of names provided coincide with the instance length.
I had to reimplement the same kind of workaround hack in section handling as
the one already performed in UnivNames because the name information is not
present in the section data structure. This deserves a FIXME.
|
|
|
|
entries
|
|
|
|
Removing a few Global.env in the way.
|
|
|
|
|
|
eg in [Class Foo (A:Type) := foo : A.] the universe should be
declared when declaring the constant [Foo] and not [foo].
|
|
|
|
|
|
Imitating the kernel in anticipation for the kernel being more obedient
|
|
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
|
|
|
|
|
|
|
|
Highly spaghetti code, hopefully works.
|
|
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
Fix #5012.
|
|
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
|
|
We address the easy ones, but they should probably be all removed.
|
|
|
|
This API is a bit strange, I expect it will change at some point.
|
|
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
|
|
Normalization sounds like it should be semantically noop.
|
|
The "Stream.Error" printer does add a period, so, the messages
themselves should not.
|
|
Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were
declared twice for all records.
Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an
observable error for monomorphic records.
|
