diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:27:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:27:09 +0200 |
| commit | 0413899668e8be15df5065abdaf1d40ad3c2c31b (patch) | |
| tree | 5d2c4671737b9d0c9eba68cdf0d16503c6e47608 /kernel/reduction.ml | |
| parent | d7db69dea59cddd3ac81ed469170fad889af4e16 (diff) | |
Fix checker to handle projections with eta and universe polymorphism correctly.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ebba23165..31c338dd9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -468,7 +468,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible - (* Eta expansion of records *) + (* Eta expansion of records *) | (FConstruct ((ind1,j1),u1), _) -> (try let v1, v2 = |