Extraction Implicits: can accept argument names instead of just positions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13109 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 3 deletions

diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index b2256c471..18828241c 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -14,6 +14,10 @@ open Vernacexpr
 open Pcoq
 open Genarg
 open Pp
+open Names
+open Nameops
+open Table
+open Extract_env
 
 let pr_mlname _ _ _ s = spc () ++ qs s
 
@@ -24,8 +28,16 @@ ARGUMENT EXTEND mlname
 | [ string(s) ] -> [ s ]
 END
 
-open Table
-open Extract_env
+let pr_int_or_id _ _ _ = function
+  | ArgInt i -> int i
+  | ArgId id -> pr_id id
+
+ARGUMENT EXTEND int_or_id
+  TYPED AS int_or_id
+  PRINTED BY pr_int_or_id
+| [ preident(id) ] -> [ ArgId (id_of_string id) ]
+| [ integer(i) ] -> [ ArgInt i ]
+END
 
 let pr_language = function
   | Ocaml -> str "Ocaml"
@@ -91,7 +103,7 @@ END
 
 VERNAC COMMAND EXTEND ExtractionImplicit
 (* Custom implicit arguments of some csts/inds/constructors *)
-| [ "Extraction" "Implicit" global(r) "[" integer_list(l) "]" ]
+| [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ]
   -> [ extraction_implicit r l ]
 END