From fbfc1ff19252520da7700341ba67a75b2e113746 Mon Sep 17 00:00:00 2001
From: bertot
Date: Mon, 10 Mar 2003 16:01:05 +0000
Subject: Remove a TODO in the translation of generic arguments:   the case of
 casted open constr.

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

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index de4821eee8..494cf593f2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1091,7 +1091,11 @@ and coerce_genarg_to_TARG x =
   | TacticArgType ->
       let t = xlate_tactic (out_gen rawwit_tactic x) in
       CT_coerce_TACTIC_COM_to_TARG t
-  | CastedOpenConstrArgType -> xlate_error "TODO: open constr"
+  | CastedOpenConstrArgType -> 
+      CT_coerce_SCOMMENT_CONTENT_to_TARG
+      	(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
+						 (out_gen
+						    rawwit_casted_open_constr x)))
   | ConstrWithBindingsArgType -> xlate_error "TODO: constr with bindings"
   | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
   | List0ArgType l -> xlate_error "TODO: lists of generic arguments"
-- 
cgit v1.2.3