Commit 1843d0c1 authored by Janno's avatar Janno

Remove leftover comments.

parent 42a8dc3a
Pipeline #7112 passed with stage
in 15 minutes and 45 seconds
......@@ -172,7 +172,6 @@ Ltac solve_closed :=
match goal with
| |- Closed ?X ?e =>
let e' := W.of_expr e in change (Closed X (W.to_expr e'));
(* apply W.is_closed_correct; vm_compute; exact I *)
apply W.is_closed_correct; exact (I <: W.is_closed X e')
end.
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
......@@ -190,7 +189,6 @@ Ltac solve_to_val :=
| |- is_Some (to_val ?e) =>
let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
apply W.to_val_is_Some, (bool_decide_unpack _);
(* vm_compute; exact I *)
match goal with [|-Is_true (@bool_decide ?P ?dec)] =>
exact (I <: Is_true (@bool_decide P dec))
end
......@@ -202,7 +200,6 @@ Ltac solve_atomic :=
match goal with
| |- Atomic ?s ?e =>
let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
(* apply W.is_atomic_correct; vm_compute; exact I *)
apply W.is_atomic_correct; exact (I <: W.is_atomic e')
end.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
......
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