From 4475bfa79f401eaa7cf9561472c5e8edb72bd8c0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 16 Jul 2002 13:43:32 +0000
Subject: petit bug lors du passage d'hugo

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

diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 3bff63100c..34b57a45c1 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -127,7 +127,7 @@ let _ = declare_summary "Extraction Inline"
 
 let extraction_inline b vl =
   let refs = List.map (fun x -> check_constant (Nametab.global x)) vl in 
-  add_anonymous_leaf (inline_extraction (true,refs))
+  add_anonymous_leaf (inline_extraction (b,refs))
 
 (*s Printing part *)
 
-- 
cgit v1.2.3