| Age | Commit message (Collapse) | Author |
|---|
|
Projection Compatibility
Reviewed-by: Zimmi48
|
|
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
|
|
Ack-by: Zimmi48
Ack-by: silene
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
White spaces are forbidden in the “&ident” syntax for ltac2 references.
|
|
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
Ack-by: herbelin
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
for integers and natural nums
|
|
complained (fixes #10580).
|
|
|
|
|
|
It has been deprecated since 8.4. The documentation was incorrect since
at least 8.5 (the last two arguments were ignored).
`Backtrack m n p` was a synonym for `BackTo m`
We also move `BackTo` handling to coqtop, since it is not meant to be
part of the document.
|
|
href: coq/coq#9651
|
|
Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are
implemented in the kernel so that they can be used by OCaml code (e.g.,
extracted code) as the other primitives.
|
|
The ExtrOCamlInt63 module can be required to map primitives from the Int63
module to their OCaml implementation (module Uint63 from the kernel).
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82
|
|
files and insert it into .rst files
Ack-by: Zimmi48
Ack-by: gares
Ack-by: ppedrot
|
|
and inserting it into the .rst files
|
|
|
|
|
|
|
|
|
|
Redefine classical real numbers as a quotient of those constructive real numbers.
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
|
|
|
|
|
|
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.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
new one
|
|
|
|
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.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: herbelin
Ack-by: jfehrle
|
|
It prints a goal given its internal goal id and the Stm state id.
|
|
This looks more principled, and doesn't require as much tinkering with
the typing implementation.
|
|
|
|
This datatype does belong to this layer.
|
|
We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:
- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
pushed upwards]
We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.
More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
|
|
in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
#10205.
Reviewed-by: cpitclaudel
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
