Commit 8ca8b776 authored by Ralf Jung's avatar Ralf Jung

handle language.of_val in solve_into_val

parent 3961c1e8
...@@ -96,6 +96,7 @@ Ltac of_expr e := ...@@ -96,6 +96,7 @@ Ltac of_expr e :=
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2) let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
| to_expr ?e => e | to_expr ?e => e
| of_val ?v => constr:(Val v (of_val v) (to_of_val v)) | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
| language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
| _ => match goal with | _ => match goal with
| H : to_val e = Some ?v |- _ => constr:(Val v e H) | H : to_val e = Some ?v |- _ => constr:(Val v e H)
| H : Closed [] e |- _ => constr:(@ClosedExpr e H) | H : Closed [] e |- _ => constr:(@ClosedExpr e H)
......
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