From bf18afeefa06e972c6cb98fa8a81ec7172fdde7f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 20 May 2014 19:56:29 +0200
Subject: Moving (e)transitivity out of the AST.

---
 parsing/g_tactic.ml4 | 2 --
 1 file changed, 2 deletions(-)

(limited to 'parsing')

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 ",";
-- 
cgit v1.2.3