| 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
```
|
| |\ \ \ \ |
|
| | | | | |\
| | | | | |
| | | | | |
| | | | | | |
(EDIT: for mutual fixpoints)
|
| | | | | | | |
|
| | |/ / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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).
|
| |/ / / |
|
| | | |
| | |
| | |
| | | |
This fixes Théo's bug on eset.
|
| |\ \ \
| | | |
| | | |
| | | | |
resolution trace
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
It has been deprecated for a while in favor of `Qed`.
|
| | | |/ / /
| |/| | |
| | | | |
| | | | | |
For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We do that by using constr_with_bindings rather than
open_constr_with_bindings (+ extra call to typeclasses in
"specialize"). If my understanding is right, the only effect would be
to succeed more in cases where it was failing (in
inh_conv_coerce_to_gen). In particular, "specialize" and
"contradiction" already have a WITHHOLES test for rejecting pending
holes.
Incidentally, this answers enhancement #5153.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Ensure in type constr_pattern that those preexisting existential
variables of the goal which do not contribute as pattern variables are
expanded: constr_pattern is not observed up to evar expansion (like
EConstr does), so we need to pre-normalize defined evars in patterns
to that matching against an EConstr works.
|
| |\ \ \
| | | |
| | | |
| | | | |
tricks available to users
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | |/ /
|/| | |
|
| | | | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |_|/ / /
|/| | | | |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
The addition to the test suite showcases the usage.
|
| |\ \ \ \ \ \
| |/ / / / /
|/| | | | | |
|
| | | | | |\ \
| | | | | | |
| | | | | | |
| | | | | | | |
with evars).
|
| | | | | |\ \ \ |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
|
| | | | | |/ / / |
|
| | | | | |/ /
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The cause was a missing evar/evar clause in ltac pattern-matching
function (constr_matching.ml).
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
let-ins
|
| | |_|_|/ / /
|/| | | | | |
|
| |\ \ \ \ \ \
| | |_|_|/ /
| |/| | | | |
|
| | | | | | | |
|
| | | |_|_|/
| |/| | |
| | | | |
| | | | | |
Add a test-suite file to be sure we won't regress silently.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.
This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.
Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
|
| |\ \ \ \ \
| |_|_|_|/
|/| | | |
| | | | | |
record fields.
|
| | |_|_|/
|/| | |
| | | |
| | | | |
Also remove obvious comments.
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
|
Pierre-Marie Pédrot
Maxime Dénès
Jason Gross
Pierre Courtieu
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre Letouzey
Gaetan Gilbert
Paul Steckler
Matthieu Sozeau