From a29b0c1bc26a6e2a37fa431e9347ed25c1bd1c2b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 16 Nov 2021 10:23:56 +0100
Subject: Maps.v: transparency of Node

Add one more `Local Transparent Node` to ensure compatibility with Coq < 8.12
---
 lib/Maps.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/Maps.v b/lib/Maps.v
index f3330776..0d83aa98 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -692,7 +692,7 @@ Module PTree <: TREE.
       forall m1 m2,
       beq m1 m2 = true <-> (forall x, beq_optA (get x m1) (get x m2) = true).
     Proof.
-Local Transparent Node.
+      Local Transparent Node.
       assert (beq_NN: forall l1 o1 r1 l2 o2 r2,
               not_trivially_empty l1 o1 r1 ->
               not_trivially_empty l2 o2 r2 ->
@@ -836,6 +836,8 @@ Local Transparent Node.
       (fun l lrec o r rrec => Node lrec (match o with None => None | Some a => f a end) rrec)
       m.
 
+  Local Transparent Node.
+
   Definition map_filter1 :=
     Eval cbv [map_filter1_nonopt tree_rec tree_rec' Node] in @map_filter1_nonopt.
 
-- 
cgit