Commit 6da0a433 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Wed Apr 10 02:24:59 CEST 2019)

parent 83178123
......@@ -530,7 +530,10 @@ type_of = yb maybeT . go
rec_subst subs (subst (Cons a') preret)
go' (Ap (Axiom t _) subs) = rec_subst subs t
rec_subst (y:t) (Bind Prod _ _ e) = rec_subst t (subst y e)
rec_subst (y:t) (Bind Prod _ tx e) = do
ty <- go y
_ <- return (convertible tx ty)^.maybeT
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