From 82a84fef19dd09c94d21bf7f69a041190e81959f Mon Sep 17 00:00:00 2001 From: Jason Hu Date: Thu, 27 Jun 2024 15:20:43 -0400 Subject: [PATCH] fix tactics (#126) --- theories/LibTactics.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/LibTactics.v b/theories/LibTactics.v index 27b1aaf3..8ed1439f 100644 --- a/theories/LibTactics.v +++ b/theories/LibTactics.v @@ -324,10 +324,10 @@ Ltac unify_args H P := let tac1 := fun H R H1 T => (let h := find_head T in unify R h; strong_apply H H1) in let tac2 := fun H R G => (let h := find_head G in unify R h; apply H; simpl) in match goal with - | H : ?R <∙> _, H1 : ?T |- _ => tac1 H R H1 T - | H : relation_equivalence ?R _, H1 : ?T |- _ => tac1 H R H1 T - | H : ?R <∙> _ |- ?G => tac2 H R G - | H : relation_equivalence ?R _ |- ?G => tac2 H R G + | H : ?R <∙> _, H1 : ?T |- _ => progress tac1 H R H1 T + | H : relation_equivalence ?R _, H1 : ?T |- _ => progress tac1 H R H1 T + | H : ?R <∙> _ |- ?G => progress tac2 H R G + | H : relation_equivalence ?R _ |- ?G => progress tac2 H R G end. @@ -340,10 +340,10 @@ Ltac unify_args H P := let tac1 := fun H R H1 T => (let h := find_head T in unify R h; strong_apply H H1) in let tac2 := fun H R G => (let h := find_head G in unify R h; apply H; simpl) in match goal with - | H : _ <∙> ?R, H1 : ?T |- _ => tac1 H R H1 T - | H : relation_equivalence _ ?R, H1 : ?T |- _ => tac1 H R H1 T - | H : _ <∙> ?R |- ?G => tac2 H R G - | H : relation_equivalence _ ?R |- ?G => tac2 H R G + | H : _ <∙> ?R, H1 : ?T |- _ => progress tac1 H R H1 T + | H : relation_equivalence _ ?R, H1 : ?T |- _ => progress tac1 H R H1 T + | H : _ <∙> ?R |- ?G => progress tac2 H R G + | H : relation_equivalence _ ?R |- ?G => progress tac2 H R G end. #[global]