diff options
Diffstat (limited to 'plugins/interface/depends.ml')
| -rw-r--r-- | plugins/interface/depends.ml | 3 |
1 files changed, 2 insertions, 1 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 |