diff options
| author | Matthieu Sozeau | 2014-11-22 17:51:43 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-11-22 17:52:29 +0100 |
| commit | 221a2ee32545e22f8002b0903b215d8c890b2125 (patch) | |
| tree | 93863e602b8daf90f5a24a79a7a6ca7b6526a4a3 /dev/include | |
| parent | 4614b430cab05f71dde87cfe2ccaa5063705ac1e (diff) | |
Fix resolve_morphism to build well-scoped terms in case some arguments
of the function are dependent.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions