From 0413899668e8be15df5065abdaf1d40ad3c2c31b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Sat, 6 Sep 2014 11:27:09 +0200
Subject: Fix checker to handle projections with eta and universe polymorphism
 correctly.

---
 kernel/reduction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/reduction.ml')

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 =
-- 
cgit v1.2.3