From f3d34e3e3add974d79d14f043c19a6d76c2b71b7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Sep 2003 11:22:20 +0000
Subject: Utilisation de noms dans 'Implicit Arguments [...]'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ec9e88c773..3ebad5ae36 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1674,7 +1674,10 @@ let xlate_vernac =
 	(reference_to_ct_ID id,
 	 match opt_positions with
 	     None -> CT_int_list[]
-	   | Some l -> CT_int_list(List.map (fun x -> CT_int x) l))
+	   | Some l ->
+	       CT_int_list
+	       (List.map (function ExplByPos x -> CT_int x | ExplByName _ ->
+		 xlate_error "TODO: explicit argument by name") l))
   | VernacReserve _ -> xlate_error "TODO: Default Variable Type"
   | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
   | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
-- 
cgit v1.2.3