| Age | Commit message (Collapse) | Author |
|---|
|
I think the usage looks cleaner this way.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
(when defining a new constant)
|
|
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.
|
|
|
|
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Before #9263 this type was returned by the STM's `parse_sentence`, but
the type was lost on the generalization to entries.
|
|
This was dead code, it was never raised ever.
|
|
records
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
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.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
declare_mutual_inductive_with_eliminations
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
Fix #8076.
|
|
|
|
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
|
|
This makes it print the warning before the definition message, so if
we run with +non-primitive-record we don't see
"""
defined foo
error could not define foo
"""
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
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>
|
|
|
|
This simplifies reasoning about the kernel code.
We still auto downgrade squashed Prop records as the code path to
avoid an error is more involved. Alternatively we could produce an
error forcing people to Unset Primitive Projections if they want a
squashed record.
|
|
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
|
|
|
|
|
|
This makes code paths clearer (we still factorize a lot of the
treatment), and we seize the opportunity to forbid anonymous
`Declare Instance` which is not a documented construction, and seems to
make little sense in practice.
|
|
|
|
|
|
|
|
We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
ML files at the root were not taken into account. Coqdep was already
doing the right thing.
|
|
|
|
|
|
This is a reworking of 7fd28dc9: instead of using words such as
"domain of", "codomain of" to refer to a position in the instance of
the original evar, we simply display the instance and the name of the
unresolved evar in this instance. This is both simpler and more
informative. (The positional words remain useful for printing the
evar_map in debugging though.)
In passing, this fixes #8369 (Not_found in printing message about an
unresolved subevar).
Incidentally add possible breaking while printing "in environment".
|
|
|
|
|
|
The situation is too unclear to make it of general use, plus it has
some issues (#9296)
I'm not deleting the warning as it can still be useful to find which
types are template for those who want to experiment.
|
