Commit c579b46c authored by Robbert Krebbers's avatar Robbert Krebbers

Avoid use of `solve_proper`.

Due to Coq bug #10480 or #10474 it actually used `Morphisms.solve_proper`
instead of the version of std++. The version in std++ can inherently
not solve this, so I changed it into a manual proof.
parent 556a5992
Pipeline #19530 passed with stage
in 9 minutes and 56 seconds
......@@ -401,7 +401,7 @@ Section infinite.
(** Properties about the [fresh] operation on finite sets *)
Global Instance fresh_proper: Proper ((@{C}) ==> (=)) fresh.
Proof. unfold fresh, set_fresh. solve_proper. Qed.
Proof. unfold fresh, set_fresh. by intros X1 X2 ->. Qed.
Lemma is_fresh X : fresh X X.
Proof.
......
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