| Age | Commit message (Collapse) | Author |
|---|
|
![proof_stack] is equivalent to the old meaning of ![proof]: the body
has type `pstate:Proof_global.t option -> Proof_global.t option`
The other specifiers are for the following body types:
~~~
![open_proof] `is_ontop:bool -> pstate`
![maybe_open_proof] `is_ontop:bool -> pstate option`
![proof] `pstate:pstate -> pstate`
![proof_opt_query] `pstate:pstate option -> unit`
![proof_query] `pstate:pstate -> unit`
~~~
The `is_ontop` is only used for the warning message when declaring a
section variable inside a proof, we could also just stop warning.
The specifiers look closely related to stm classifiers, but currently
they're unconnected. Notably this means that a ![proof_query] doesn't
have to be classified QUERY.
![proof_stack] is only used by g_rewrite/rewrite whose behaviour I
don't fully understand, maybe we can drop it in the future.
For compat we may want to consider keeping ![proof] with its old
meaning and using some new name for the new meaning. OTOH fixing
plugins to be stricter is easier if we change it as the errors tell us
where it's used.
|
|
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
|
|
|
|
We never use this id in rewrite.ml so don't bother threading it around.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
To prevent confusion, forbidding a mix of the "injection term as pat1
... patn" and of the "injection term as [= pat1 ... patn]" syntax: If
a "[= ...]" occurs, this should be a singleton list of patterns.
|
|
Using pstate makes no sense for printing global stuff
|
|
|
|
|
|
It's used a few times in the stdlib (a couple of which need no other
change when removing the !) and not at all throughout our CI.
Considering that I think it's fair enough to remove it.
|
|
This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.
The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.
We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.
Fixes #3632 #3890 #4638.
|
|
|
|
|
|
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
|
|
|
|
|
|
|
|
|
|
|
|
I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.
|
|
One other call still remains, but will require to refactor some
section-handling code.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
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 future uses of this token for non integer numerals.
|
|
|
|
Instead of just string (and empty strings for tokens without payload)
|
|
|
|
We add state handling to tactics.
TODO:
- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac
|
|
Previously, they were hard-wired in the ML code.
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
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: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
Deprecate the old syntax.
The documented syntax was using a with clause which is more standard with a hint database
than the using clause that was actually implemented.
|
|
Supersedes #8718.
|
|
Ack-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
I think the usage looks cleaner this way.
|
|
In order to do so we place the polymorphic status and name in the
read-only part of the monad.
Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.
Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.
Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.
|
|
Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).
Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
|
|
The semantics is obviously that it is an error if not at least one
occurrence is found (natural semantics for rewriting for
example).
|
|
This is only used for debugging, if a user wants more feedback she can turn
on the option. Conversely, it has a cost for any tactic script, so it is
wiser to disable it by default.
|
|
Fixes #7769: Better control over ltac backtraces.
Fixes #7385: Tactic allocates gigabytes of RAM.
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
|
|
the intros tactic to its own subsection. Add grammar and examples.
|
|
|
|
|
|
(in case of side effects)
Also:
Fix #4781
Fix #4496
|
