From 5ec6f9c21e446b869a11320b69bfdd51f204c691 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 10 Jun 2010 17:43:38 +0000
Subject: 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
---
 plugins/extraction/table.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/extraction/table.mli')

diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 04d90b881..b215e373e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -149,7 +149,10 @@ val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
 val extract_inductive :
   reference -> string -> string list -> string option -> unit
-val extraction_implicit : reference -> int list -> unit
+
+
+type int_or_id = ArgInt of int | ArgId of identifier
+val extraction_implicit : reference -> int_or_id list -> unit
 
 (*s Table of blacklisted filenames *)
 
-- 
cgit v1.2.3