From d6b1274515890c22930ae54ff0b7bb492eebd622 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 22 Aug 2020 15:55:17 -0700
Subject: Modify Init/Wf.v to compile with -mangle-names

---
 theories/Init/Wf.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index a305626eb3..60200ae0f6 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -85,8 +85,7 @@ Section Well_founded.
 
   Scheme Acc_inv_dep := Induction for Acc Sort Prop.
 
-  Lemma Fix_F_eq :
-   forall (x:A) (r:Acc x),
+  Lemma Fix_F_eq (x:A) (r:Acc x) :
      F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r.
   Proof.
    destruct r using Acc_inv_dep; auto.
@@ -104,7 +103,7 @@ Section Well_founded.
 
   Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
   Proof.
-   intro x; induction (Rwf x); intros.
+   intro x; induction (Rwf x); intros r s.
    rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
    apply F_ext; auto.
   Qed.
-- 
cgit v1.2.3