aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/tacexpr.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 5a7a20ef63..223ece63be 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -157,7 +157,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
(* Equivalence relations *)
| TacSymmetry of 'nam clause_expr
- | TacTransitivity of 'trm option
(* Equality and inversion *)
| TacRewrite of evars_flag *