| Age | Commit message (Collapse) | Author |
|---|
|
expected.
|
|
context obtained by ltac pattern-matching)
|
|
|
|
|
|
|
|
|
|
|
|
Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability.
Tough maybe it signals too much an unelegant debugging flavor?
|
|
The main fix is to use is_ident_soft. The rest of the commit is to
provide something a bit more appealing than "?M-1".
|
|
It seems that reinstalling gcc can leave Cygwin in a strange state,
where invocations of gcc fail suddenly. I haven't figure out exactly
why, but this seems to fix it.
|
|
|
|
It was introduced in 8.5 for compatibility with a 8.4 bug.
|
|
|
|
|
|
|
|
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
top of the linking chain.
|
|
from location in file
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Inductive-keyworded record failing even on non-dependent goal)
|
|
|
|
work better on them
|
|
|
|
|
|
|
|
anonymous variables)
|
|
|
|
This changes the implementation of "constructor" from
constructor 1 + ... + constructor n + fail
to
constructor 1 + ... + constructor n.
|
|
|
|
- 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.
|
|
|
