From 5f7281089fd0a101acb365cfcd432a06b7bfe680 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Mar 2017 16:35:07 -0400 Subject: More compatibility for etransitivity --- src/Util/Tactics/ETransitivity.v | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src') 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.. ]. -- cgit v1.2.3