From 65f99a024ee3ff2694fe4e2774e42503c81dd462 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 28 Jul 2020 17:33:02 -0700
Subject: Modify Init/Specif.v to compile with -mangle-names

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

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 4ff007570e..1fb6dabe6f 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -765,7 +765,7 @@ Section Dependent_choice_lemmas.
     exists f.
     split.
     - reflexivity.
-    - induction n; simpl; apply proj2_sig.
+    - intro n; induction n; simpl; apply proj2_sig.
   Defined.
 
 End Dependent_choice_lemmas.
-- 
cgit v1.2.3