From 71cdbefb8ce0f20e21f2c1dcd02f914fad24614c Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 12 Oct 2004 09:10:29 +0000
Subject: option -no-hash-consing pour supprimmer le hash-consing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6201 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index c2d83a71cd..93a90380c8 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -179,7 +179,7 @@ let (in_constant, out_constant) =
     export_function = export_constant } 
 
 let hcons_constant_declaration = function
-  | DefinitionEntry ce ->
+  | DefinitionEntry ce when !Options.hash_cons_proofs ->
       let (hcons1_constr,_) = hcons_constr (hcons_names()) in
       DefinitionEntry
        { const_entry_body = hcons1_constr ce.const_entry_body;
-- 
cgit v1.2.3