aboutsummaryrefslogtreecommitdiff
path: root/grammar
diff options
context:
space:
mode:
Diffstat (limited to 'grammar')
-rw-r--r--grammar/q_coqast.ml41
1 files changed, 0 insertions, 1 deletions
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) ->