diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/depends.ml | 9 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 6 |
2 files changed, 3 insertions, 12 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index 16357fc472..39eaa0b98b 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -210,7 +210,7 @@ let rec depends_of_rawconstr rc acc = match rc with | RLambda (_, _, _, rct, rcb) | RProd (_, _, _, rct, rcb) | RLetIn (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc) - | RCases (_, rco, tmt, cc) -> + | RCases (_, _, rco, tmt, cc) -> (* LEM TODO: handle the cc *) (Option.fold_right depends_of_rawconstr rco (list_union_map @@ -221,13 +221,6 @@ let rec depends_of_rawconstr rc acc = match rc with acc)) | RLetTuple (_,_,(_,rco),rc0,rc1) -> depends_of_rawconstr rc1 (depends_of_rawconstr rc0 (Option.fold_right depends_of_rawconstr rco acc)) - | RLetPattern (_, tmt, cc) -> - (* LEM TODO: handle the cc *) - (fun (rc, pp) acc -> - Option.fold_right (fun (_,ind,_,_) acc -> (IndRef ind)::acc) (snd pp) - (depends_of_rawconstr rc acc)) - tmt - acc | RIf (_, rcC, (_, rco), rcT, rcF) -> let dorc = depends_of_rawconstr in dorc rcF (dorc rcT (dorc rcF (dorc rcC (Option.fold_right dorc rco acc)))) | RRec (_, _, _, rdla, rca0, rca1) -> let dorca = array_union_map depends_of_rawconstr in diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 2219e327ca..aa7a50dce2 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -360,8 +360,6 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b) | CLetIn(_, v, a, b) -> CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b) - | CLetPattern(_, v, a, b) -> - error "TODO: xlate_formula let | pattern" | CAppExpl(_, (Some n, r), l) -> let l', last = decompose_last l in CT_proj(xlate_formula last, @@ -379,8 +377,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function (xlate_formula f, List.map xlate_formula_expl l')) | CApp(_, (_,f), l) -> CT_appc(xlate_formula f, xlate_formula_expl_ne_list l) - | CCases (_, _, [], _) -> assert false - | CCases (_, ret_type, tm::tml, eqns)-> + | CCases (_, _, _, [], _) -> assert false + | CCases (_, _, ret_type, tm::tml, eqns)-> CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm, List.map xlate_matched_formula tml), xlate_formula_opt ret_type, |