From 6f53ffee4a1c85ac07e82c65d31de0d2a367566b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 20 Aug 2013 08:22:39 +0000
Subject: Attempt to restore hash-consing of opaque terms

 Without this, the stdlib vo files are +30% larger

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16707 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declareops.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index ac3aad15e7..76d9876c49 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -89,10 +89,9 @@ let hcons_const_def = function
     let constr = force l_constr in
     Def (from_val (Term.hcons_constr constr))
   | OpaqueDef lc ->
-    if Future.is_val lc then
-      let constr = force_opaque (Future.force lc) in
-      OpaqueDef (Future.from_val (opaque_from_val (Term.hcons_constr constr)))
-    else OpaqueDef lc
+    OpaqueDef
+      (Future.chain ~pure:true lc
+         (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc))))
 
 let hcons_const_body cb =
   { cb with
-- 
cgit v1.2.3