| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
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.
|
|
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).
|
|
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Fixes #9494.
Was failing with "Cannot create self-referring hypothesis" when
the generated name equaled the eqn.
|
|
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.
|
|
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>
|
|
the intros tactic to its own subsection. Add grammar and examples.
|
|
|
|
|
|
|
|
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
This should improve correctness and will be needed for the PRs that
remove global access to the proof state.
|
|
|
|
|
|
|
|
|
|
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
Also remove a few undocumented settings
|
|
|
|
Returning a writer insinuates that it is not exactly the same as the
writer which was passed as argument, but that is incorrect.
|
|
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
|
|
|
|
|
|
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
This is inspired and an alternative to #8981. We consolidate the "open
proof" exception, allowing clients to explicitly capture it and
removing some ugly duplicated code in the way.
The `Solve Obligation tac` semantics are then tweaked as to removed
the wide-scope "catch-all" and indeed will now relay errors in `tac`
as it will only absorb tactics that don't error but fail to close the
goal such as `auto`. For the rest of the cases, we introduce a
warning, and may move to a full error in later releases.
We also remove an unnecessary `tclCOMPLETE` call to code that will
actually call `close_proof`. In this case, it is better to delegate
error management to the core function.
Some error messages have changed [as we consolidate two error paths]
so this PR may require adjustment in that area.
|
|
|
|
Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
|
|
|
|
|
|
This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.
|
|
|
|
Detected when making Typing check universe instances.
|
|
|
