| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
This fixes #6378. Previously the ML module was never declared anywhere.
Thanks to @cmangin for the pointer.
|
| |/
|
|
| |
Fixes GH#6384 and GH#6385.
|
| |
|
|
|
|
|
|
| |
In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.
Universes of a monomorphic reference [c] are considered to appear in
the term [c].
|
| |
|
|
|
|
|
|
| |
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
|
| |\
| |
| |
| | |
#3125)
|
| | |
| |
| |
| |
| |
| |
| | |
In particular singleton inductive types are considered injectable,
even in the absence of the option "Set Keep Proof Equalities".
This fixes #3125 (and #4560, #6273).
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Note that this makes the following syntax valid:
Axiom foo@{i} bar : Type@{i}.
(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
|
| |/
|
|
|
|
| |
This fixes BZ#5717.
Also add a test and fix a changed test.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Moving at the same to a passing "env sigma" style rather than passing
"gl". Not that it is strictly necessary, but since we had to move
functions taking only a "sigma" to functions taking also a "env", we
eventually adopted the "env sigma" style. (The "gl" style would have
been as good.)
This answers wish #4717.
|
| | |/
|/|
| |
| |
| | |
With help from Guillaume (see discussion at
https://github.com/coq/coq/issues/6191).
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| | |
The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
(clause "where" with implicit arguments)
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
unbound rel
|
| | |_|_|/
|/| | | |
|
| | | | |
| | | |
| | | |
| | | | |
Fixes #6165.
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | | |
When an evar is undefined we need to substitute inside the evar instance.
With help from @herbelin and @psteckler to identify the issue from a
large test case.
|
| |/ / |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We improve one step further the heuristics to sort out if a variable
is a notation variable or a named variable.
This allows to support the following which was still failing.
Reserved Notation "# x" (at level 0).
Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I).
We rely here on the property that a binding variable of same name as a
notation variables is itself considered bound by the notation.
This becomes however to be a bit tricky for sorting out if the
variable has to be output to the glob file or not.
|
| |\ \
| |/
|/| |
|
| |\ \
| | |
| | |
| | | |
alphabet).
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We refine the criterion for selecting a projection. Before PR#924 it
was alphabetic (i.e. morally "random" up to alpha-conversion). After
PR#924 it was chronological.
We refine a bit more by giving priority to simple projections when
they exist over projections which include an evar instantiation (and
which may actually be ill-typed).
|
| | |/
|/|
| |
| | |
Adding a file fixing #5996 and which uses this feature.
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
variables).
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This concerns pr_value and message_of_value.
This has a few consequences. For instance, no more ad hoc message "a
term" or "a tactic", when not enough information is available for
printing, one gets a generic message "a value of type foobar".
But we also have more printers, satisfying e.g. request #5786.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We fix by interpreting the pattern in "change pat with term" in strict
mode by using the same interning code as for "match goal" (even if the
pattern is dropped afterwards).
|
| | |/ /
|/| |
| | |
| | | |
This fixes also #5731, #6035, #5364.
|
| |\ \ \
| |/ /
|/| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
| | | | |
|
| |/ / |
|
| |\ \
| | |
| | |
| | | |
clause of an inductive definitions
|
| | | | |
|
| | | |
| | |
| | |
| | | |
The test suite cases are preserved until the feature is actually removed.
|
| |\ \ \
| |_|/
|/| | |
|
| |\ \ \
| | | |
| | | |
| | | | |
"_something")
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
inductive definition)
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
BZ#4852)
|
| | |_|_|/ /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
148)
For compatibility, this extra feature of omega could be disabled via
Unset Omega UseLocalDefs.
Caveat : for now, real let-ins inside goals or hyps aren't handled, use
some "cbv zeta" reduction if you want to get rid of them. And context
definitions whose types aren't Z or nat are ignored, some manual "unfold"
are still mandatory if expanding these definitions will help omega.
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
BZ#5757)
|
Maxime Dénès
Jason Gross
Tej Chajed
Gaëtan Gilbert
Matthieu Sozeau
Hugo Herbelin
Matthieu Sozeau
Théo Zimmermann
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Pierre Letouzey