Commit 450f6388 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Thu May 2 01:48:51 CEST 2019)

parent 74760859
...@@ -565,7 +565,7 @@ type_of = yb maybeT . go ...@@ -565,7 +565,7 @@ type_of = yb maybeT . go
rec_subst (y:t) (Bind Prod _ tx e) = do rec_subst (y:t) (Bind Prod _ tx e) = do
ty <- go y ty <- go y
(_,dx) <- return (convertDelta ty tx)^.maybeT (dx,_) <- return (convertDelta ty tx)^.maybeT
guard (dx<=0) guard (dx<=0)
rec_subst t (subst y e) rec_subst t (subst y e)
rec_subst [] x = return x rec_subst [] x = return x
......
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