From c82bea6f76ad0b6ea57cda027cc49ec009850a48 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 12 Sep 2020 17:13:21 -0700
Subject: Modify Arith/Factorial.v to compile with -mangle-names

---
 theories/Arith/Factorial.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 0871c4af67..f87d7e810a 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -33,7 +33,7 @@ Qed.
 
 Lemma fact_le n m : n <= m -> fact n <= fact m.
 Proof.
-  induction 1.
+  induction 1 as [|m ?].
   - apply le_n.
   - simpl. transitivity (fact m). trivial. apply Nat.le_add_r.
 Qed.
-- 
cgit v1.2.3