diff options
Diffstat (limited to 'plugins/extraction/g_extraction.ml4')
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 6cba83ef9..76b435410 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -20,7 +20,6 @@ open Genarg open Stdarg open Pp open Names -open Nameops open Table open Extract_env @@ -35,7 +34,7 @@ END let pr_int_or_id _ _ _ = function | ArgInt i -> int i - | ArgId id -> pr_id id + | ArgId id -> Id.print id ARGUMENT EXTEND int_or_id PRINTED BY pr_int_or_id |