diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-24 02:01:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-28 18:52:55 +0200 |
| commit | efa921c807e48cfc19943d2bfd7f4eb11f8f9e09 (patch) | |
| tree | 5984eeff9ad901d9b59bcc76618c5ff184b1b45d /pretyping/pretyping.mllib | |
| parent | 820dd1fa1c5d701c5f9af6e456b066d97a0d0499 (diff) | |
Extra check for indirect dependency when abstracting a term which is
not a variable, in the future objective to factorize code between
"generalize dependent" and "set", "destruct", etc.
Diffstat (limited to 'pretyping/pretyping.mllib')
0 files changed, 0 insertions, 0 deletions