diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/depends.ml | 3 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index a0cbe22b36..16357fc472 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -340,7 +340,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacClear _ | TacClearBody _ | TacMove _ - | TacRename _ -> acc + | TacRename _ + | TacRevert _ -> acc (* Constructors *) | TacLeft cb diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c5a8c756a8..2219e327ca 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1187,6 +1187,7 @@ and xlate_tac = let idl' = List.map xlate_hyp idl in CT_clear (CT_id_ne_list (xlate_hyp id, idl')) | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'" + | TacRevert _ -> xlate_error "TODO: revert" | (*For translating tactics/Inv.v *) TacInversion (NonDepInversion (k,idl,l),quant_hyp) -> CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp, @@ -1248,6 +1249,7 @@ and xlate_tac = (CT_formula_list (List.map xlate_formula (out_gen (wit_list0 rawwit_constr) args))) + | TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal" | TacExtend (_,id, l) -> print_endline ("Extratactics : "^ id); CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l)) |