diff options
| author | Arnaud Spiwack | 2014-08-01 19:14:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:59 +0200 |
| commit | 94b201b0a7b03978d96b8f8c9d631e4fa4bda4b0 (patch) | |
| tree | 998601ebfb4ad8163bd6c3fb81fabe331c154947 /kernel/type_errors.ml | |
| parent | b240b7d0cfd6233dcb0ba0e3b98354c78c23a0d4 (diff) | |
Faster uconstr.
Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions