diff options
Diffstat (limited to 'plugins/interface')
| -rw-r--r-- | plugins/interface/depends.ml | 3 | ||||
| -rw-r--r-- | plugins/interface/xlate.ml | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml index 445b193f81..9e649a5a2f 100644 --- a/plugins/interface/depends.ml +++ b/plugins/interface/depends.ml @@ -357,7 +357,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of (* Equivalence relations *) | TacReflexivity | TacSymmetry _ -> acc - | TacTransitivity c -> depends_of_'constr c acc + | TacTransitivity (Some c) -> depends_of_'constr c acc + | TacTransitivity None -> acc (* Equality and inversion *) | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index bff8cae260..9629fa923c 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -1066,7 +1066,8 @@ and xlate_tac = (out_gen (wit_list1 rawwit_ident) l))) | TacReflexivity -> CT_reflexivity | TacSymmetry cls -> CT_symmetry(xlate_clause cls) - | TacTransitivity c -> CT_transitivity (xlate_formula c) + | TacTransitivity (Some c) -> CT_transitivity (xlate_formula c) + | TacTransitivity None -> xlate_error "TODO: etransitivity" | TacAssumption -> CT_assumption | TacExact c -> CT_exact (xlate_formula c) | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c) |