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.

---
 grammar/q_coqast.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 6a413ca313..e152cdd7f4 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -409,7 +409,6 @@ let rec mlexpr_of_atomic_tactic = function
 
   (* Equivalence relations *)
   | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
-  | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
   | Tacexpr.TacAuto (debug,n,lems,l) ->
-- 
cgit v1.2.3