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 /checker/term.ml | |
| parent | d7db69dea59cddd3ac81ed469170fad889af4e16 (diff) | |
Fix checker to handle projections with eta and universe polymorphism correctly.
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/term.ml b/checker/term.ml index 1b8177325..30142c2cd 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -392,6 +392,7 @@ let compare_constr f t1 t2 = Array.equal f tl1 tl2 && Array.equal f bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 + | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2 | _ -> false let rec eq_constr m n = |