diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-16 19:34:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-16 22:28:42 +0200 |
| commit | 3c2723f77f5ab070f8232ce0cc626875120cfe41 (patch) | |
| tree | e52b630876715c95e44b294e9c2dc17ab6ceff83 /dev | |
| parent | 4158d921d506ce931ec940c55005f0698be9616b (diff) | |
In convert_concl/convert_hyp: nf_enter -> enter.
(Maybe one of the source of inefficiency introduced on Oct 9 - see e.g. CoLoR.)
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions