Commit 2aa844c9 authored by Robbert Krebbers's avatar Robbert Krebbers

Let set_solver/set_unfold only touch Prop hyps.

This is needed to use coq-stdpp in developments with -type-in-type
as set_unfold will otherwise unify with any hyp, causing the
set_solver tactic to break.
parent a0ce0937
......@@ -270,9 +270,13 @@ End set_unfold_list.
Ltac set_unfold :=
let rec unfold_hyps :=
try match goal with
| H : _ |- _ =>
apply set_unfold_1 in H; revert H;
first [unfold_hyps; intros H | intros H; fail 1]
| H : ?P |- _ =>
lazymatch type of P with
| Prop =>
apply set_unfold_1 in H; revert H;
first [unfold_hyps; intros H | intros H; fail 1]
| _ => fail
end
end in
apply set_unfold_2; unfold_hyps; csimpl in *.
......
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