Commit 9883e152 authored by Robbert Krebbers's avatar Robbert Krebbers

Better use of unicode in type classes test file.

parent 3c0bfaec
......@@ -9,7 +9,7 @@ From stdpp Require Import prelude.
[2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
*)
Lemma test_setoid_rewrite :
exists R, @Reflexive Prop R /\ R = iff.
R, @Reflexive Prop R R = iff.
Proof.
eexists. split.
- apply _.
......
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