From b1e012f41ef94dae2e57a616011af39b44b56b9d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 27 Jun 2019 12:15:49 +0200
Subject: [extraction] Remove not very useful call to dumpglob.

The old code was conditionally dumping and catching `Not_found`, as
noted by Gaëtan Gilbert on #10433:

> we could just remove the dump, the sibling functions
> (`full_extraction`, etc...) don't bother to dump for instance.
---
 plugins/extraction/extract_env.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 31dcfdd168..7ee8d7f342 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -645,7 +645,6 @@ let separate_extraction lr =
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r =
-  Vernacentries.dump_global CAst.(make (Constrexpr.AN r));
   match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
-- 
cgit v1.2.3