diff options
| -rw-r--r-- | contrib/extraction/table.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 *) |