diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-10 12:59:44 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-10 13:01:24 +0200 |
| commit | af767e36829ada2b23f5d8eae631649e865392ae (patch) | |
| tree | fc850ddd224e3f6ed5acd6417d27bb71ff07dcbf /proofs/clenvtac.ml | |
| parent | 6624459e492164b3d189e3518864379ff985bf8c (diff) | |
Parsing and printing of primitive projections, fix buggy behavior when
implicits do not allow to parse as an application and cleanup code.
Diffstat (limited to 'proofs/clenvtac.ml')
0 files changed, 0 insertions, 0 deletions