diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-29 17:42:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-29 17:42:13 +0200 |
| commit | a273df3af0e4315fd792efd83b9365320531111d (patch) | |
| tree | 08b521031bfd19ffbe49f50ba3b711e939f09bfb /parsing/parsing.mllib | |
| parent | 85f95cc9f11dc630e59f3a13362e151134ce92ea (diff) | |
When building on-the-fly elimination principles, set the predicates universe variable
as algebraic so it can disappear from the proof (it always gets substituted away from
the term). This means less spurious universes remaining in proof terms.
Diffstat (limited to 'parsing/parsing.mllib')
0 files changed, 0 insertions, 0 deletions