diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 82ddf46a2d..df1557481b 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -574,12 +574,8 @@ let separate_extraction lr = (*s Simple extraction in the Coq toplevel. The vernacular command is \verb!Extraction! [qualid]. *) -let dump_global r = - let gr = Smartlocate.global_with_alias r in - Dumpglob.add_glob (loc_of_reference r) gr - let simple_extraction r = - dump_global r; + Vernacentries.dump_global (Misctypes.AN r); match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> |