From 8a65852d1b39137898bddbaf7cf949bceeb4a574 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 2 Aug 2017 15:45:12 +0200
Subject: [PATCH] Fix compilation

---
 FiniteSets/disjunction.v                | 6 +++---
 FiniteSets/fsets/properties_decidable.v | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/FiniteSets/disjunction.v b/FiniteSets/disjunction.v
index fe8c1dd..f279413 100644
--- a/FiniteSets/disjunction.v
+++ b/FiniteSets/disjunction.v
@@ -176,10 +176,10 @@ Section hPropLattice.
       associative_max := _ ;
       idempotent_min := _ ;
       idempotent_max := _ ;
-      neutralL_min := _ ;
-      neutralR_min := _ ;
+      neutralL_max := _ ;
+      neutralR_max := _ ;
       absorption_min_max := _ ;
       absorption_max_min := _
   }.
   
-End hPropLattice.
\ No newline at end of file
+End hPropLattice.
diff --git a/FiniteSets/fsets/properties_decidable.v b/FiniteSets/fsets/properties_decidable.v
index 3080817..9cf3ac3 100644
--- a/FiniteSets/fsets/properties_decidable.v
+++ b/FiniteSets/fsets/properties_decidable.v
@@ -208,8 +208,8 @@ Section SetLattice.
       associative_max := _ ;
       idempotent_min := _ ;
       idempotent_max := _ ;
-      neutralL_min := _ ;
-      neutralR_min := _ ;
+      neutralL_max := _ ;
+      neutralR_max := _ ;
       absorption_min_max := _ ;
       absorption_max_min := _
     }.