diff options
author | Jason Gross <jgross@mit.edu> | 2017-03-31 16:35:07 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-03-31 16:35:07 -0400 |
commit | 5f7281089fd0a101acb365cfcd432a06b7bfe680 (patch) | |
tree | fc9a629e831dd0d3915ffa89288da4fa2b34f162 | |
parent | f89309d47a1f4095430c984b4ab81c804a9263ae (diff) |
More compatibility for etransitivity
-rw-r--r-- | src/Util/Tactics/ETransitivity.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/Util/Tactics/ETransitivity.v b/src/Util/Tactics/ETransitivity.v index c6fe59318..16f26c8e3 100644 --- a/src/Util/Tactics/ETransitivity.v +++ b/src/Util/Tactics/ETransitivity.v @@ -1,14 +1,18 @@ Require Import Coq.Classes.RelationClasses. Tactic Notation "etransitivity" open_constr(y) := + intros; let R := match goal with |- ?R ?x ?z => constr:(R) end in let x := match goal with |- ?R ?x ?z => constr:(x) end in let z := match goal with |- ?R ?x ?z => constr:(z) end in let pre_proof_term_head := constr:(@transitivity _ R _) in let proof_term_head := (eval cbn in pre_proof_term_head) in refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ]. -Tactic Notation "etransitivity" := etransitivity _. +(** We call [Coq.Init.Notations.etransitivity] for compatibility + because it's more powerful than [etransitivity _] in some cases, + e.g., when things need to be unfolded. *) +Tactic Notation "etransitivity" := Coq.Init.Notations.etransitivity. Tactic Notation "etransitivity_rev" uconstr(y) := [ > etransitivity y; cycle 1.. ]. -Tactic Notation "etransitivity_rev" := etransitivity_rev _. +Tactic Notation "etransitivity_rev" := [ > etransitivity; cycle 1.. ]. Ltac transitivity_rev y := [ > transitivity y; cycle 1.. ]. |