aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_tactic.ml42
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4ac7a5bffe..3e80c99f5a 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -652,8 +652,6 @@ GEXTEND Gram
(* Equivalence relations *)
| IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl
- | IDENT "transitivity"; c = constr -> TacTransitivity (Some c)
- | IDENT "etransitivity" -> TacTransitivity None
(* Equality and inversion *)
| IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";