diff options
| author | Hugo Herbelin | 2014-10-20 23:34:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-20 23:46:40 +0200 |
| commit | da462f8a2b59a3d5ddd9f09add8a75f8e2624c9a (patch) | |
| tree | 195e24524bee1e699238d12881f4a0082d307cb8 /dev/base_include | |
| parent | 98f3abb83a26b85092140e8850fd372622f24bdb (diff) | |
Removing re-typecheking from "refine" in no-check mode of the new
convert_concl/convert_hyp. This was actually probably the main source
of inefficiency introduced on Oct 9 (see e.g. CoLoR), rather than
nf_enter, as suspected in 3c2723f.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions