| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
top of the linking chain.
|
|
from location in file
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Inductive-keyworded record failing even on non-dependent goal)
|
|
|
|
work better on them
|
|
|
|
|
|
|
|
anonymous variables)
|
|
|
|
|
|
- timing needs time and python
- check for compiled files without source looks in the install
directory (except for make -f Makefile.ci which doesn't check), as
such the install directory has been renamed to _install_ci and isn't
searched.
|
|
A trick in counting spaces in a format was making the empty notation
not behaving correctly.
|
|
|
|
Conditions for printing 'pat were incomplete.
|
|
|
|
Was causing a failure to print recursive binders used twice or more in
the same notation.
|
|
When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.
|
|
For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_".
|
|
|
|
|
|
artificially restricted to a non-empty context).
|
|
It hasn't been necessary since
6aad0d9cd2104b5343ed7c831a4ad0bbe34007cb introduced $(INSTALLLIB)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This prevents seeing things like MsgDirectory which are actually
intended to be two distinct words.
|
|
|
|
|
|
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
|
|
|
|
|
|
|
|
