diff options
| author | Pierre-Marie Pédrot | 2017-09-08 19:02:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-08 19:21:24 +0200 |
| commit | 555a7cf0ce4457ecfbf68cd12dd0e801728f6662 (patch) | |
| tree | b81a2b74a8abaa0a7160097cb86c9ecbe48d761a /kernel/type_errors.mli | |
| parent | 2b66bf0083fd85cf2fc983dbca75b848194f897f (diff) | |
Using a dedicated argument for tactic quotations.
This prevents having to go through an expensive phase of goal-building, when
we can simply type-check the term.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions