Commit b82651fb authored by Armaël Guéneau's avatar Armaël Guéneau

Small fix

parent 1aa50cba
......@@ -1124,7 +1124,7 @@ Ltac affine_base :=
*)
Ltac affine :=
match goal with
| |- affine _ => affine_base; typeclasses eauto with affine
| |- affine _ => affine_base; try (typeclasses eauto with affine)
end.
......@@ -2575,7 +2575,7 @@ Proof using.
rewrite star_assoc. exists~ h1 h2.
auto.
intros x. hchange (Qle' x). hchange~ (Qle x).
set (H' := \GC) at 1 2. hsimpl. subst H'. affine.
set (H' := \GC) at 1 2. hsimpl; subst H'; affine.
apply~ local_erase.
Qed.
......
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