Commit 46dba44e authored by Benoit Viguier's avatar Benoit Viguier

Merge remote-tracking branch 'upstream/master'

parents 332cf0a8 2aa844c9
Pipeline #4185 failed with stage
in 0 seconds
......@@ -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