From 7eeec8f82d96a71929289b0b9401a1b96e1d3dda Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 10:26:28 +0100
Subject: More compact representation for evar resolvability flag.

This patch was proposed by JH in bug report #4547.
---
 pretyping/typeclasses.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3be98a1ae2..bb475cc554 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -495,15 +495,18 @@ let is_instance = function
 let resolvable = Store.field ()
 
 let set_resolvable s b =
-  Store.set s resolvable b
+  if b then Store.remove s resolvable
+  else Store.set s resolvable ()
 
 let is_resolvable evi =
   assert (match evi.evar_body with Evar_empty -> true | _ -> false);
-  Option.default true (Store.get evi.evar_extra resolvable)
+  Option.is_empty (Store.get evi.evar_extra resolvable)
 
 let mark_resolvability_undef b evi =
-  let t = Store.set evi.evar_extra resolvable b in
-  { evi with evar_extra = t }
+  if is_resolvable evi = b then evi
+  else
+    let t = set_resolvable evi.evar_extra b in
+    { evi with evar_extra = t }
 
 let mark_resolvability b evi =
   assert (match evi.evar_body with Evar_empty -> true | _ -> false);
-- 
cgit v1.2.3