| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
|
|
|
|
| |
Redefining adjust_subst_to_rel_context from instantiate_context who
was hidden in inductiveops.ml, renamed the latter into
subst_of_rel_context_instance and moving them to Vars. The new name
highlights that the input is an instance (as for applist) and the
output a substitution (as for substl). This is a clearer unified
interface, centralizing the difficult de-Bruijn job in one place. It
saves a couple of List.rev.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Related questions:
- What balance to find between precision and conciseness?
- What convention to follow for typesetting the different components
of the documentation is unclear?
New tentative type substl to emphasize that substitutions (for substl)
are represented the other way round compared to instances for
application (applist), though there are represented the same way
(i.e. most recent/dependent component on top) as instances of evars
(mkEvar).
Also removing unused subst*_named_decl functions (at least
substnl_named_decl is somehow non-sense).
|
| |
|
| |
|
| |
|
|
|
|
|
| |
next to each other, waiting for possible integration into a more
uniform API.
|
|
|
|
|
| |
cleaning the interfaces is eventually easier. Here, adding
find_mrectype_vect to simplify vnorm.ml.
|
| |
|
|
|
|
| |
characters.
|
| |
|
|
|
|
|
|
| |
Actually, we never mix the various uses of each dynamic type created through
the Dyn module. To enforce this statically, we functorize the Dyn module so
that we recover a fresh instance at each use point.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
It was not used in Coq codebase, and the only known user was ssreflect up
to commit 95354e0dee.
|
| |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
constraints at the time of Next Obligation/Solve Obligations so that
interleaving definitions and obligation solving commands works properly.
|
| |
| |
| |
| |
| |
| |
| | |
using the wrong context.
This is very bad style but currently unavoidable, at least we don't
throw an anomaly anymore.
|
| |
| |
| |
| | |
projections (off by default).
|
| |
| |
| |
| | |
using dot notation.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
longer stable w.r.t. equality constraints as the universe graph will
choose different canonical levels depending on the equalities given to
it (l = r vs r = l).
|
| | |
|
| | |
|
| | |
|
|\| |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
| |
| |
| |
| | |
valid (when Top.i is global and hence > Set).
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
The fix was actually elementary. The lexer comes with a function to
compare parsed tokens against tokens of the parsing rules. It is
enough to have this function considering an ident in a parsing rule to
be equal to the corresponding string parsed as a keyword.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The nametab in which the error message is printed is not the one in
which the error message happens.
This reveals a weakness in the fix_exn code: the fix_exn function should
be pure, while in some cases (like this one) uses the global state (the
nametab) to print a term in a pretty way (the shortest non-ambiguous name
for constants).
This patch makes the externalization phase (used by term printing)
resilient to an incomplete nametab, so that printing a term in the
wrong nametab does not mask the original error.
|
| | |
|
| |
| |
| |
| |
| |
| | |
Instead of accumulating constraints which are not present in the original
graph, we parametrize the equality function by a function actually merging
those constraints in the current graph. This prevents doing the work twice.
|
|\| |
|
| | |
|