diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-06 15:25:18 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-06 15:25:18 +0000 |
| commit | 145bd37bb83b41749b7e95f535569c249e98df38 (patch) | |
| tree | 5c15dfc148296077614f17b24b755df7dea11afc /plugins/extraction | |
| parent | 0f3147561c3558e2c6d5c0ec1d100ec746aa716e (diff) | |
Vecnacentries.dump_global silently ignores exceptions
So PrintName and Extraction dump globals when they exist
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15691 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
| -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 82ddf46a2..df1557481 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],[] -> |