diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-21 00:16:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:01:21 +0100 |
| commit | e3cefca41b568b1e517313051a111b0416cd2594 (patch) | |
| tree | c21a1fbcc2cbd6fe41cfd691df2103ff1f445989 /kernel/reduction.mli | |
| parent | 6899d3aa567436784a08af4e179c2ef1fa504a02 (diff) | |
Slight simplification of the code of primitive projection (in relation
to c71aa6b and 6ababf) so as to rely on generic functions rather than
re-doing the de Bruijn indices cooking locally.
Diffstat (limited to 'kernel/reduction.mli')
0 files changed, 0 insertions, 0 deletions