| Age | Commit message (Collapse) | Author |
|---|
|
And document the error message.
|
|
We alert users that `Vernacstate.Proof_global` is a Coq internal
module and should not be used to workaround lack of state threading.
|
|
We perform some cleanup and remove dependency of `proofs/` on
`interp/`, which seems logical.
In fact, `interp` + `parsing` are quite self-contained, so if there is
interest we could also make tactics to depend directly on proofs.
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: vbgl
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
This removes various compatibility notations.
Closes #8374
This commit was mostly created by running `./dev/tools/update-compat.py
--release`. There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.
The update to CHANGES.md was manual.
|
|
Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.
This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`
See examples of each use case in the next two commits.
|
|
In anticipation of an extension from natural numbers to other numeral
constants.
|
|
In anticipation of future uses of this token for non integer numerals.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Instead of just string (and empty strings for tokens without payload)
|
|
Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals
Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t
Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")
|
|
This is a fairly small cleanup on the `vernac_interp` function, which
makes code cleaner and for example would allow to have `Load` inside
`Load`. [Not that we would ever want that]
|
|
This is the right thing to do until we refine the program architecture
a bit to use EConstr.
Closes #9163 .
|
|
|
|
In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.
|
|
We try to do a bit of cleanup for the `with_fail` function, this still
is delicate code.
|
|
Not sure the warning is worth the extra parameter.
|
|
This is used in the test-suite to check that a proof is closed; I am
not sure we'd like to keep this patch tho: the non-failing semantics
seems saner for IDEs.
[main users are in `test-suite/ide`]
|
|
In that case the terminator and proof object have to be supplied in
the ?proof argument, or else we get an anomaly.
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
|
|
We add state handling to tactics.
TODO:
- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac
|
|
|
|
This is in view of the 8.10 release, after which we will remove the
option and the `VtUnknown` classification.
|
|
Previously, they were hard-wired in the ML code.
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jfehrle
|
|
|
|
|
|
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.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: vbgl
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
record
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jashug
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
|
|
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
|
|
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.
|
|
|
|
|
|
Supersedes #8718.
|
