From eca149363d20d94198a4b1e1ae4f9f964e468098 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 21 Jan 2021 16:07:24 +0100
Subject: Define `fold_ind_aux` and `fold_ind` transparently

The extraction mechanism wants to extract them (because they are in
Type, probably).  The current opaque definition causes a warning at
extraction-time.
---
 lib/Maps.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/Maps.v b/lib/Maps.v
index 092ab6ea..c617d488 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1349,7 +1349,7 @@ Proof.
   + inv NOREPET. auto.
   + apply FINAL. auto.
   + apply IHl. auto. inv NOREPET; auto.
-Qed.
+Defined.
 
 Theorem fold_ind:
   P m_final (T.fold f m_final init).
@@ -1364,7 +1364,7 @@ Proof.
   rewrite T.fold_spec. apply X.
   intros; simpl. rewrite <- List.in_rev.
   split. apply T.elements_complete. apply T.elements_correct.
-Qed.
+Defined.
 
 End TREE_FOLD_IND.
 
-- 
cgit