diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-09 15:06:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-09 15:06:44 +0000 |
| commit | a580a7a07da8651887c6fb386bd9af55bbe673a2 (patch) | |
| tree | 4233682720571f3fa09fba77bb31e446dc6203e1 /contrib | |
| parent | 51cd60453da3f1fe136904404046098d9c4f1cc3 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 3e4d486a8..afa9226e1 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, |