| Age | Commit message (Collapse) | Author |
|---|
|
This allows to embed Ltac2 functions manipulating Ltac1 values as simple
Ltac1 values.
|
|
This should have the same semantics, it is just a matter of moving the
responsibility of evaluating the thunk from the Ltac1 application tactic to
the quotation.
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
|
|
This is a syntactic sugar that is compiled away to a simple case analysis.
|
|
typ_param -> ltac2_typevar,
tac2expr -> ltac2_expr
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Negative values had no meaning there.
Those were spotted by Hugo Herbelin while reviewing #12979 .
|
|
|
|
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: proux01
Ack-by: silene
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: MSoegtropIMC
Reviewed-by: gares
|
|
It seems that nobody tried to write a parameterized type with more than one
parameter since this was causing a syntax error. LL(1) being great, we work
around the issue by factorizing the syntax with the generic parentheses and
decide the validity after parsing.
|
|
|
|
At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
Current backtraces for tactics leave a bit to desire, for example
given the program:
```coq
Lemma u n : n + 0 = n.
rewrite plus_O_n.
```
the backtrace stops at:
```
Found no subterm matching "0 + ?M160" in the current goal.
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```
Backtrace information `?info` is as of today optional in some tactics,
such as `tclZERO`, it doesn't cost a lot however to reify backtrace
information indeed in `tclZERO` and provide backtraces for all tactic
errors. The cost should be small if we are not in debug mode.
The backtrace for the failed rewrite is now:
```
Found no subterm matching "0 + ?M160" in the current goal.
Raised at file "pretyping/unification.ml", line 1827, characters 14-73
Called from file "pretyping/unification.ml", line 1929, characters 17-53
Called from file "pretyping/unification.ml", line 1948, characters 22-72
Called from file "pretyping/unification.ml", line 2020, characters 14-56
Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73
Called from file "proofs/clenv.ml", line 254, characters 12-58
Called from file "proofs/clenvtac.ml", line 95, characters 16-53
Called from file "engine/proofview.ml", line 1110, characters 40-46
Called from file "engine/proofview.ml", line 1115, characters 10-34
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```
which IMO is much better.
|
|
|
|
|
|
Thread the `ev` (an `evar_flag`) appropriately through `intros0`.
Discussed on https://gitter.im/coq/coq?at=5eacace7f0377f16316083b8.
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
|
|
If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
|
|
|
|
This completes a pure Dune bootstrap of Coq.
There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.
TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.
Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
|
|
|
|
|
|
If we need more fine-tuning we should manage the warnings with the
standard Coq mechanism.
|
|
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
|
|
We remove Coq's wrapper over gramlib's grammar constructors.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
That is, it contains the type of the binder so as not to rely on the relevance
explicitly.
|
|
For robustness and it is better to leave it opaque. Users are not supposed to
fiddle with it.
|
|
Add headers to a few files which were missing them.
|
