| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: JasonGross
|
|
The grammar engine has the great idea to silently delete empty levels on rule
removal. Since Ltac2 level 4 is initially empty, it means that when backtracking
on the loading of the Ltac2 plugin, the grammar would be in a state where the
level 4 was not there at all.
There is a dedicated API for that situation in Pcoq, but it is kind of crazy
that we have to use this kind of workaround when the problem is clearly that
gramlib has the wrong default.
Fixes #14156: Ltac2 broken with async.
|
|
Reviewed-by: JasonGross
|
|
Reviewed-by: JasonGross
Ack-by: jfehrle
|
|
Reviewed-by: JasonGross
|
|
Reviewed-by: ppedrot
|
|
Fixes #11683.
|
|
All other equality functions are called "equal" but this one was called "eq".
We add a deprecated alias for backward compatibility.
|
|
For some reason I was confusing the position and the level in the previous
version of the code.
Fixes #11866: Ltac2 Notations do not respect precedence.
|
|
Reviewed-by: JasonGross
|
|
passing one single hintdb is not quite the right API, we should
pass a transparent state instead, but that would require an API
for manipulating hintdbs and transparent states, postponing
|
|
Grammar vernacular
Reviewed-by: JasonGross
|
|
Fixes #14092: Print Grammar ltac2 should exist.
|
|
Reviewed-by: JasonGross
|
|
Fixes #14083
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Partial fix of #14013.
|
|
Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented.
Fixes #13996: missing Ltac1.to_ident.
|
|
Previously, `Array.init` was computing the first element of the array
twice, resulting in exponential overhead in the number of recursive
nestings of `Array.init`. Notably, since `Array.map` is implemented in
terms of `Array.init`, this exponential blowup shows up in any term
traversal based on `Array.map` over the arguments of application nodes.
Fixes #14011
|
|
Fixes #14003: Ltac2 redefinition check is broken.
|
|
Reviewed-by: JasonGross
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48
|
|
|
|
As a bonus ltac2 can produce bullet suggestions.
|
|
Fixes #13963
|
|
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
|
|
Reviewed-by: gares
|
|
|
|
Fixes #10095: Get list of constructors of Inductive.
|
|
Fixes #12806: Ltac2 Notation's open_constr should accept scope stacks.
|
|
Fixes #12785: Ltac2 Performance Overhead.
|
|
Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.
This should be 1:1 equivalent to the previous code, we are just moving code
around.
|
|
|
|
|
|
Reviewed-by: JasonGross
Reviewed-by: MSoegtropIMC
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
It provides an abstract type of well-typed format strings, a scope to parse
them and a minimal printf-like API.
|
|
into `pat:`
Ack-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
|
|
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.
|
