diff options
| -rw-r--r-- | plugins/extraction/extract_env.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 7 | ||||
| -rw-r--r-- | toplevel/vernacentries.mli | 2 |
3 files changed, 7 insertions, 8 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],[] -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a4a14b7b30..7a786ce92b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -421,9 +421,10 @@ let smart_global r = gr let dump_global r = - let gr = Smartlocate.smart_global r in + try + let gr = Smartlocate.smart_global r in Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr - + with _ -> () (**********) (* Syntax *) @@ -1347,7 +1348,7 @@ let vernac_print = function | PrintNamespace ns -> print_namespace ns | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ()) | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) - | PrintName qid -> msg_notice (print_name qid) + | PrintName qid -> dump_global qid; msg_notice (print_name qid) | PrintGraph -> msg_notice (Prettyp.print_graph()) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index dbceaaaa1e..b49c01f896 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -13,6 +13,8 @@ open Vernacexpr open Constrexpr open Misctypes +val dump_global : Libnames.reference or_by_notation -> unit + (** Vernacular entries *) val show_script : unit -> unit |