| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| | |
|
| | |/
|/| |
|
| |\ \ |
|
| | | | |
|
| | |/
|/| |
|
| | |
| |
| |
| | |
This file doesn't want to leave us.
|
| | |
| |
| |
| |
| |
| | |
This fixes bug #5380 in particular.
More generally, tags were not updated to the correct default value
if the corresponding line in the configuration file was missing.
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.
This change is necessary in order to fix bug ####.
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Due to the situation explained in bug 5360, error printing in
ide_slave results in an anomaly. We fix that by properly processing
the error.
This fixes BZ#5524, however BZ#5525 , still applies.
|
| |/ / |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
There was a mistake in the conflict resolution of merge
6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 which wrongly undid the the
deletion of the file `ide/texmacspp.ml` in 6a412da , fixing here and
sorry for the problem.
|
| |\ \
| | |
| | |
| | | |
more uniform
|
| | | |
| | |
| | |
| | | |
This allows to share the test for possible relocalisation done in envars.ml.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
They were not used for looking for coqide files in the situation when
the effective installation path happens to be exactly the installation
path proposed by default, while relevant files were however (possibly)
installed in these directories.
|
| |/ /
| |
| |
| |
| |
| |
| |
| | |
Deprecations which can't be fixed in 4.02.3 are locally wrapped with
[@@@ocaml.warning "-3"]. The only ones encountered are
- capitalize to capitalize_ascii and variants. Changing to ascii would
break coqdoc -latin1 and maybe other things though.
- external "noalloc" to external [@@noalloc]
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
The .mli only acknowledges the current API. I'm not guilty your honor!
|
| | | |/ / |
|
| | |/ /
| | |
| | |
| | | |
It has been deprecated for a while in favor of `Qed`.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
So far this part of the system has shown little utility other than
having developers put time to fix it every time they change something
in the system.
I have never seen this functionality used in the wild, and a large
part of the vernac was marked TODO. Given that we have automatic
methods to provide this functionality these days (PPX), we remove
Texmacspp.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Off by default.
+ small refactoring of emacs hacks in printer.ml.
|
| | |\ \ |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
let-ins
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | |/ /
| |/| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| | | | |
| | | |
| | | |
| | | | |
Now it is a private field, locations are optional.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This warning is a special case as it happens outside the execution
context.
We could move the check inside, but instead we opt for the simpler
solution of properly setting the warning target.
|
| | |/ / / |
|
Maxime Dénès
Matej Košík
Pierre-Marie Pédrot
Paul Steckler
Emilio Jesus Gallego Arias
Cyprien Mangin
Amin Timany
Jason Gross
Hugo Herbelin
Gaëtan Gilbert
Enrico Tassi
Pierre Courtieu