diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ecedc9002d..0efdbbb6b5 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -606,7 +606,6 @@ let extraction_inline b l = let print_extraction_inline () = let (i,n)= !inline_table in let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in - msg (str "Extraction Inline:" ++ fnl () ++ Refset'.fold (fun r p -> |