| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
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
|
|
|
|
|
|
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
|
|
|
|
These were found with the following command:
$ git grep "1999-" | grep -v "2019"
|
|
Remove other types of lines before copyright headers.
|
|
|
|
|
|
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: tlringer
|
|
|
|
This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual
After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.
Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.
|
|
Reviewed-by: cpitclaudel
|
|
This allows to refer to them from other part of the manual without any ambiguity.
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: cpitclaudel
|
