diff options
| author | Pierre-Marie Pédrot | 2018-08-14 17:34:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-26 15:51:10 +0200 |
| commit | f4ca5fa41eff290a1815e83fe920fe3bc4422907 (patch) | |
| tree | 6138f92a5392fa73c1d3b0e357265b1ce4e2d636 /Makefile.ide | |
| parent | 8c3f395e52020f82822100730026a950c3653c8c (diff) | |
Inline the definition of CClosure.mk_clos_deep.
An important part of this function was dead code, due to the fact it was only
used for whd evaluation of specific shapes of constr.
Diffstat (limited to 'Makefile.ide')
0 files changed, 0 insertions, 0 deletions