| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
Inductive-keyworded record failing even on non-dependent goal)
|
|
|
|
work better on them
|
|
|
|
|
|
|
|
anonymous variables)
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Because the argument given to refine may mess with the evarmap, the goal being
refined can be solved by side-effect after the term filler is computed. If this
happens, we simply don't perform the refining operation.
|
|
|
|
|
|
|
