diff options
| author | Pierre-Marie Pédrot | 2014-04-01 18:12:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-01 18:55:28 +0200 |
| commit | 502e61ec1ac488dd430ce6654c7a6947c6f7d1c3 (patch) | |
| tree | 9270e2bbbb0d131a174301b51b6bf20731f40a2e /kernel/nativecode.ml | |
| parent | fed97ad8d6c34b6a577f8477a03200b1056dbc46 (diff) | |
Evars introduced by Proofview refining are flagged as GoalEvar. For some
reasons, some code depends on it.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions