Commit 68254659 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix compilation with Coq 8.4pl4.

parent 044d309d
......@@ -68,7 +68,7 @@ Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
(f : A B) `{!Surjective (=) f} : { g : B A & Cancel (=) f g }.
Proof.
exists (λ y, choose (λ x, f x = y) (surjective f y)).
intros y. by rewrite (choose_correct _ (surjective f y)).
intros y. by rewrite (choose_correct (λ _, _) (surjective f y)).
Qed.
(** ** Instances *)
......
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