| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
This is what has always been used, so it doesn't represent a functional
change.
This is just a preliminary patch, but many more possibilities could be
done wrt tags.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Applications of it were not clear/unproven, it made printers more
complex (as they needed to be functors) and as it lacked examples it
confused some people.
The printers now tag unconditionally, it is up to the backends to
interpreted the tags.
Tagging (and indeed the notion of rich document) should be reworked in
a follow-up patch, so they are in sync, but this is a first step.
Tested, test-suite passes.
Notes:
- We remove the `Richprinter` module. It was only used in the
`annotate` IDE protocol call, its output was identical to the normal
printer (or even inconsistent if taggers were not kept manually in
sync).
- Note that Richpp didn't need a single change. In particular, its
main API entry point `Richpp.rich_pp` is not used by anyone.
|
| |
|
|
|
| |
The miscellaneous `msg_*` cleanup patches have finally enforced this
invariant.
|
| |
|
|
|
|
| |
We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| | |
The `a.[i] <- x` notation is deprecated and we were getting a couple
of warnings.
|
| |\ \ |
|
| |\ \ \ |
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The "theories/Logic/PropExtensionalityFacts.v" file was:
- compiled
- used in several places
but not actually installed.
This commit fixes that.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
|
| |\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Coq.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.
- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional changes.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change, one extra copy introduced but it seems hard to
avoid.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change, one extra copy introduced but it seems hard to
avoid.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional changes, only a minor copy on a deprecated output
option.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change, even if we could optimize `blanch_utf8_string` a
bit more by using `String.init`.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
We add a more convenient API to create identifiers from mutable
strings. We cannot solve the `String.copy` deprecation problem until
we enable `-safe-string`.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
The `emitcodes` string type was used in both a functional and an
imperative way, so we have to handle it with care in order to preserve
the previous optimizations and semantics.
|
| |\ \ \ \ \ \ \ \ \ |
|
| | |_|_|_|_|_|/ / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Augments "A fully applied tactic is expected" with the list of missing
arguments to the tactic. Addresses [bug
5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change, we create the new string beforehand and
`id_of_string` will become a noop with `-safe-string`.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change.js
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional change.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
No functional changes.
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|/
|/| | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | |_|_|_|_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
It was always set to `greedy:true`.
|
| | |_|_|/ / / / / / / / / /
|/| | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
We now allow the user to overlay contribution repositories and
branches by adding their own rules to `ci-basic-overlay.sh`.
This just provides very basic support.
|
| |/ / / / / / / / / / / /
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
The code was assuming that Proofview.tclFOCUS could raise a
CList.IndexOutOfRange exception but this isn't the case.
The focusing functions already catch this exception and
raises an algebraic exception within the tactic mechanism.
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
This commit also documents the behavior of said function;
and fix the location of the ssreflect clone to an absolute
path (this is now necessary).
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Matej Kosik
Hugo Herbelin
Tej Chajed
Théo Zimmermann