Commit 8105adfe authored by Raphael Cauderlier's avatar Raphael Cauderlier

Remove an unused context variable

parent 75dd3560
......@@ -33,7 +33,7 @@ def mrun : A : prop -> mtactic A -> proof A.
[a] mrun _ (mret _ a) --> a.
def mbind : A : prop -> B : prop -> mtactic A -> (proof A -> mtactic B) -> mtactic B.
[a,f,t] mbind _ _ (mret _ t) f --> f t
[f,t] mbind _ _ (mret _ t) f --> f t
[B,t] mbind _ B (mraise _ t) _ --> mraise B t.
def mtry : A : prop -> mtactic A -> (exc -> mtactic A) -> mtactic A.
......
Markdown is supported
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