| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
line -sprop-cumulative
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Add headers to a few files which were missing them.
|
|
Cleanup: IMHO most of the re-raises here are not worth it.
|
|
|
|
|
|
|
|
The current behaviour could be considered as sub-optimal, but it probably
doesn't matter in practice as this happens when serializing side-effects.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
Instead, we export in Safe_typing the current module declaration.
|
|
|
|
preparation for direct discharge
|
|
~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
|
|
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
|
|
This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.
We may instead consider using `type t = section * section list` which
needs some boilerplate to update.
|
|
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
```
|
|
|
|
Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
|
|
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.
|
|
Rather than in typeops
|
|
If you have access to a kernel name you also should have the
environment in which it is defined, barring hacks. In order to
disfavor hacks we make the standard lookups raise anomalies so that
people are forced to admit they rely on the internals of the
environment.
We find that hackers operated on the code for side effects, for
finding inductive schemes, for simpl and for Print Assumptions. They
attempted to operate on funind but the error handling code they wrote
would have raised another Not_found instead of being useful.
All these uses are indeed hacky so I am satisfied that we are not
forcing new hacks on callers.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
|
|
|
|
This ensures that side-effect declarations come with their body, in prevision
of the decoupling of the Safe_typign API for CEP 40.
|
|
proofs.
We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.
|
|
We separate the Term_typing inference API into two functions, one to
typecheck just the immediate part of an entry, and another one to check
after the fact that a delayed term is indeed a correct proof for an opaque
entry.
This commit is mostly moving code around, this should be 1:1 semantically.
|
|
The information is already there.
At some point we may want to clean up the Lib API to reduce redundancy
wrt kernel functions like [sections_are_opened], but I'm not doing now
as it would conflict with https://github.com/coq/coq/pull/10670
|
|
Reviewed-by: gares
|
|
|
|
We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.
Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.
|
|
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
|
|
This allows to remove the double declaration of monomorphic universes of
discharged section constants. This also makes it much clearer that only
the first declaration of a constant is allowed to declare delayed
constraints.
As a nice bonus, this simplifies the Opaqueproof API.
|
|
This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
|
|
Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
|
|
For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
|
|
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
The caller should push them first
|
|
|
