From 7008fddba4b0a1ac9e46c0bf5af8ea09839232c8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Oct 2008 16:16:43 +0000
Subject: Suite 11472

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

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8c470f1bd7..77cde062ff 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1304,11 +1304,13 @@ and coerce_genarg_to_TARG x =
 	     (CT_coerce_ID_to_ID_OR_INT id))
   | IntroPatternArgType ->
       xlate_error "TODO"
-  | IdentArgType ->
+  | IdentArgType true ->
       let id = xlate_ident (out_gen rawwit_ident x) in
 	CT_coerce_FORMULA_OR_INT_to_TARG
 	  (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
 	     (CT_coerce_ID_to_ID_OR_INT id))
+  | IdentArgType false ->
+      xlate_error "TODO"
   | VarArgType ->
       let id = xlate_ident (snd (out_gen rawwit_var x)) in
 	CT_coerce_FORMULA_OR_INT_to_TARG
@@ -1402,11 +1404,13 @@ let coerce_genarg_to_VARG x =
 	        (CT_coerce_ID_to_ID_OPT id))
   | IntroPatternArgType ->
       xlate_error "TODO"
-  | IdentArgType ->
+  | IdentArgType true ->
       let id = xlate_ident (out_gen rawwit_ident x) in
       CT_coerce_ID_OPT_OR_ALL_to_VARG
 	      (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
 	        (CT_coerce_ID_to_ID_OPT id))
+  | IdentArgType false ->
+      xlate_error "TODO"
   | VarArgType ->
       let id = xlate_ident (snd (out_gen rawwit_var x)) in
       CT_coerce_ID_OPT_OR_ALL_to_VARG
-- 
cgit v1.2.3