| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | |
|
| | |/
|/|
| |
| | |
Fixes BZ#5726.
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| |\ \ \ \
| |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Fixes #6490.
`prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`,
and adjusted to work with econstr.
This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where
`has_nodep_prod_after` counts both products and let-ins, but was only
being passed `mib.mind_nparams`, which does not count let-ins.
Replaced with (Context.Rel.length mib.mind_params_ctxt).
|
| | |/
|/|
| |
| |
| |
| |
| | |
We simply use a record and pack the rel and var substitutions in it. We also
properly compose variable substitutions.
Fixes #6534: Fresh variable generation in case of clash is buggy.
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Universe instances were lost during constructions of the canonical instance.
|
| |/ /
| |
| |
| |
| | |
This is useful for tactics that run a bunch of tests and need to display
the profile for each of them.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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).
|
Maxime Dénès
Tej Chajed
Cyprien Mangin
Jasper Hugunin
Pierre-Marie Pédrot
Jason Gross
Gaëtan Gilbert
Matthieu Sozeau
Hugo Herbelin
Matthieu Sozeau