| Age | Commit message (Collapse) | Author |
|---|
|
Instead we store that data in the native code that was generated in adapt
the compilation scheme accordingly. Less indirections and less imperative
tinkering makes the code safer.
The global symbol table was originally introduced in #10359 as a way not to
depend on the Global module in the generated code. By storing all the
native-related information in the cmxs file itself, this PR also makes other
changes easier, such as e.g. #13287.
|
|
|
|
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
|
|
|
|
This is O(n) instead of O(n log n) and should be more efficient in practice.
|
|
We continue to push state layers upwards, in preparation of a
functional vernacular interpretation.
Now we move `States` and `Printmod` which messes with the global
state as to temporarily create envs with modules.
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
|
|
Reviewed-by: ejgallego
Reviewed-by: jfehrle
|
|
line -sprop-cumulative
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
In particular, the error messages do not mention anymore the notion of
bool-valued options, since these are documented as flags and work
quite differently from the rest of options.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
Add headers to a few files which were missing them.
|
|
|
|
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: Zimmi48
Reviewed-by: ppedrot
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Instead of various termops and globnames aliases.
|
|
|
|
|
|
Reviewed-by: maximedenes
|
|
|
|
|
|
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
|
|
|
|
~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
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
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
|
|
Same justification as the change in implementation of Summary.
|
|
No need to deploy an existential type machinery when we already know this type
in advance.
|
|
For historical reasons we were wrapping the data stored in the summary objects
with dynamic type casts. There is no reason to do so since we have a proper
Dyn API. Furthermore, this had a small runtime cost when we knew that it was
never going to fail.
|
|
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
```
|
|
Rather than in typeops
|
|
|
|
This ensures that side-effect declarations come with their body, in prevision
of the decoupling of the Safe_typign API for CEP 40.
|
|
There are no more users.
|
|
|
|
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
|
|
There were 2:
- when declaring a constraint to avoid monomorphic constraint
referring to polymorphic univs, this check is redundant with the
check in Section.ml
- when declaring a universe context to avoid redeclaring universes,
this is not necessary after recent commits.
|
|
sections
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
