Modify Bool/BoolEq.v to compile with -mangle-names

coq · Dec 16, 2020 · 4c4fb14 · 4c4fb14
1 parent 0f8d574
commit 4c4fb14
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
@@ -46,7 +46,7 @@ Section Bool_eq_dec.
 
   Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}.
   Proof.
-    intros.
+    intros x y.
     exists (beq x y).
     constructor.
   Defined.