Commit 74760859 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Thu May 2 01:47:27 CEST 2019)

parent 5bbdcafd
......@@ -565,7 +565,8 @@ type_of = yb maybeT . go
rec_subst (y:t) (Bind Prod _ tx e) = do
ty <- go y
_ <- return (convertDelta ty tx)^.maybeT
(_,dx) <- return (convertDelta ty tx)^.maybeT
guard (dx<=0)
rec_subst t (subst y e)
rec_subst [] x = return x
rec_subst _ _ = zero
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment