| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
short econstr-cleaning of record.ml
|
| |\ \
| | |
| | |
| | | |
ssreflect and coq code
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
```
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
|
| | | | |/ / / |
|
| |\ \ \ \ \ \
| |_|_|/ / /
|/| | | | |
| | | | | | |
recursive notations) (bis)
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | |/ /
| | | | |/| |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The new function is interp_glob_closure which is basically a renaming
and generalization of interp_uconstr.
Note a change of semantics that I could however not observe in
practice.
Formerly, interp_uconstr discarded ltac variables bound to names for
interning, but interp_constr did not. Now, both discard them.
We also export the new interp_glob_closure.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We want to avoid capture in "Inductive I {A} := C : forall A, I".
But in "Record I {A} := { C : forall A, A }.", non recursivity ensures
that no clash will occur.
This fixes previous commit, with which it could possibly be merged.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Was failing e.g. with
Inductive foo {A : Type} : Type := { Foo : foo }.
Note: the test-suite was using the bug in coindprim.v.
|
| | | | | | |/
| | | | |/|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
For instance, the following was failing to use the implicitness of n:
Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We get rid of a complex function doing both an incremental comparison
and an effect on names (Notation_ops.compare_glob_constr).
For the effect on names, it was actually already done at the time of
turning glob_constr to notation_constr, so it could be skipped here.
For the comparison, we rely on a new incremental variant of
Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the
artificial recursivity in mk_glob_constr_eq).
Seizing the opportunity to get rid of catch-all clauses in
pattern-matching (as advocated by Maxime). Also make indentation
closer to the one of other functions.
|
| | | | |/ /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This was preventing to work examples such as:
Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
|
| | | | |/ |
|
| | | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
There was an extra trailing space in #680.
Now things display as, e.g.,
```
TEST bugs/opened/3754.v
TEST bugs/opened/4803.v (-compat 8.4)
```
instead of
```
TEST bugs/opened/3754.v ( )
TEST bugs/opened/4803.v (-compat 8.4 )
```
|
| | |/
| |
| |
| | |
We only want an absolute path, no need to follow symlinks.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).
Incidentally updating output of Show output test (evar numbers shifted).
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| |\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
It used to generate only .cmo (the packed one).
While this works if the plugin has no external dependencies,
it does not if it does.
The bug affected only bytecode builds
|
| | | | | | |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| | |_|/
|/| |
| | |
| | | |
There is still however a failure with "rmdir --ignore-fail-on-non-empty".
|
| |\ \ \
| |_|/
|/| |
| | | |
resolution trace
|
| | |/
|/| |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This makes the following work correctly:
make only TGTS="foo bar" -j2
note that
make foo bar -j2
is not doing what you think
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
Restores compatibility with 8.6
|
| | | | | | | |
|
| | |_|/ / /
|/| | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
with binders)
|
| |\ \ \ \ \ \ |
|
| | |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | | |
It has been deprecated for a while in favor of `Qed`.
|
Maxime Dénès
Jason Gross
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Pierre Courtieu
Hugo Herbelin
Enrico Tassi
Théo Zimmermann
Paul Steckler