From a580a7a07da8651887c6fb386bd9af55bbe673a2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 9 Sep 2003 15:06:44 +0000
Subject: Ajout construction If primitive dans constr_expr et rawconstr

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3e4d486a8f..afa9226e11 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -323,6 +323,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		   CT_if(xlate_formula_opt po,
                    xlate_formula c,xlate_formula b1,xlate_formula b2)		
    | CLetTuple (_,l, (na,po), c, b) -> xlate_error "LetTuple: TODO"
+   | CIf (_,c, (na,None), b1, b2) ->
+		   CT_if(ctv_FORMULA_OPT_NONE,
+                   xlate_formula c,xlate_formula b1,xlate_formula b2)
+   | CIf (_,c, (na,Some p), b1, b2) -> xlate_error "If: TODO"
 
    | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
        CT_inductive_let(xlate_formula_opt po,
-- 
cgit v1.2.3