Commit caf434e7 authored by Janno's avatar Janno

Fix cast in `solve_as_val`.

Implicit typeclass instances are going to be really annoying if we
actually end up adopting these casts.
parent 059a095c
......@@ -226,7 +226,10 @@ Ltac solve_as_val :=
match goal with
| |- AsVal ?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 _); exact (I <: bool_decide (is_Some (W.to_val e')))
apply W.to_val_is_Some, (bool_decide_unpack _);
match goal with [|-Is_true (@bool_decide ?P ?dec)] =>
exact (I <: Is_true (@bool_decide P dec))
Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment