Commit 5d673f75 authored by Heiko Becker's avatar Heiko Becker

Remove unnecessary print

parent ea902e6d
......@@ -82,8 +82,6 @@ Notation "'rlet' x ':=' u 'in' t" := (resultBind u (fun x => t))
(only parsing, at level 0, t at level 200).
Notation "'ret' x" := (resultReturn x) (only parsing, at level 0 ).
Check (rlet x := (Succes true) in match x with | _ => ret true end).
Ltac optionD :=
match goal with
|H: context[resultBind ?v ?f] |- _ =>
......
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