| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
| |
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
next to each other, waiting for possible integration into a more
uniform API.
|
| | |
|
| | |
|
| | |
|
|
|
together with the tactic monad.
The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.
|
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès