diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 3 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
3 files changed, 5 insertions, 3 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c0a3f2e770..d5d32ce5b5 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -616,7 +616,8 @@ GEXTEND Gram (* Equivalence relations *) | IDENT "reflexivity" -> TacReflexivity | IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl - | IDENT "transitivity"; c = constr -> TacTransitivity c + | IDENT "transitivity"; c = constr -> TacTransitivity (Some c) + | IDENT "etransitivity" -> TacTransitivity None (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 357a572be4..bdd9241e3c 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -844,7 +844,8 @@ and pr_atom1 = function (* Equivalence relations *) | TacReflexivity as x -> pr_atom0 x | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls - | TacTransitivity c -> str "transitivity" ++ pr_constrarg c + | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c + | TacTransitivity None -> str "etransitivity" (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a494738f9c..606b652c26 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -413,7 +413,7 @@ let rec mlexpr_of_atomic_tactic = function (* Equivalence relations *) | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >> | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> - | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >> + | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >> (* Automation tactics *) | Tacexpr.TacAuto (n,lems,l) -> |