Compatible with coq-master

coq-community · Nov 13, 2024 · 1fc1c88 · 1fc1c88
1 parent 84fd7ce
commit 1fc1c88
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/prelude.v b/theories/prelude.v
@@ -15,8 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq.
 Require Import Eqdep ClassicalFacts.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -71,7 +71,7 @@ Proof. by []. Qed.
 
 (* rewrite rule for propositional symmetry *)
 Lemma sym A (x y : A) : x = y <-> y = x.
-Proof. by []. Qed.
+Proof. by split. Qed.
 
 (* selecting a list element *)
 (* should really be in seq.v *)