diff options
| author | Matthieu Sozeau | 2014-09-06 11:27:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-06 11:46:04 +0200 |
| commit | 5d888e0f4943877df04114a0513d70687d9b2c11 (patch) | |
| tree | 5823fc10dad7d6dc852ab04c0e7e603ca5f67bb7 | |
| parent | 0413899668e8be15df5065abdaf1d40ad3c2c31b (diff) | |
Fix checker to handle projections with eta and universe polymorphism correctly,
simplifying conversion code.
| -rw-r--r-- | checker/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 0bf5ae32fe..b8677f5aaa 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -473,7 +473,7 @@ let fconv cv_pb env t1 t2 = with NotConvertible -> let open Pp in if !Flags.debug then ( - Pp.ppnl (str " conversion failed: "); + Pp.ppnl (str " conversion failed on: "); Print.print_pure_constr t1; Pp.ppnl (str " and "); Print.print_pure_constr t2); |