| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
| |
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
|
|
|
| |
This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
|
| |
|
|
|
|
|
|
|
| |
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
|
| |
|
| |
|
|
|
|
| |
A non empty dir detected as an empty one.
|
| |
|
|
|
|
|
|
| |
This is useful for PIDE based interfaces, since they can
build hyperlinks out of .glob files and let the
user jump to the corresponding .v files
|
| |
|
|
|
|
| |
Solves an efficiency problem in Makefiles generated by coq_makefile.
|
| |
|
| |
|
| |
|
|
|
|
| |
This is a follow-up on Pierre's 5d80a385.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
#3802.)
|
|
|
|
| |
removing the need of thread creation in the interface.
|
|
|
|
| |
grammar in campl4
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
from v8.4)
- For the style of identifiers, coqdoc was using a 'type' attribute of
tag <span>. But this attribute isn't a legal attribute of tag <span>
according to the xhtml norm. Instead, I propose to use 'title' for that.
The coqdoc.css now supports both approaches.
- The names of inner links (cross references #foo) were
containing arbitrary characters (in the case of a notation string).
For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x">
Instead, when strange characters are detected, we now hash the
string via Digest, and use this hexa hash as html label.
- And some whitespace before />
|
|
|
|
| |
documentation en ligne)
|
| |
|
|
|
|
|
|
|
|
| |
to the first -I option.
Fortunately, with -I option, only one file can be found by occurrence
of the option, so on the contrary of -Q/-R options for v files, the
order is not file-system dependent.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Commit 3e972b3ff8e532be233f70567c87512324c99b4e renamed coq.el,
coq-db.el, coq-syntax.el to gallina.el, gallina-db.el,
gallina-syntax.el without fixing up any of the references. Commit
30b58d43e48569afb50a35d3915ec7d453a61f5d only fixed up some of them.
Here are some more (hopefully all of them).
Signed-off-by: Anders Kaseorg <andersk@mit.edu>
|
|
|
|
| |
I'm not sure that coqdep and coqtop understand them correctly anyway ...
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
These plugins, like coqidetop, stmworkertop and tacworkertop are
intended for toploop replacements (see -toploop command line option).
With this commit coq_makefile can be used as the build system for
any user-interface-specific plugins.
|
| |
|
|
|
|
|
|
|
|
|
| |
This reverts commit 60c390951cb2d771c16758a84bf592d06769da14.
The reason is that execvp exists on windows but is "non blocking".
So coqc would detach "coqtop -compile" and make would fail trying
to step to the next target before "coqtop -compile" terminates (because
coqc did terminate already).
|
|
|
|
| |
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
|
|
|
| |
Just like the [Record] keyword allows only non-recursive records.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
|
|
|
| |
Conflicts:
tools/coqdep_lexer.mll
|
| |
|
| |
|
|
|
|
|
| |
- The state machine gets kind of complex
maybe it should become a parser at some point?
|