From 3cb40ccb9ee1372c3e220d6a1da9dcae9c6a7dc7 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 25 Dec 2024 01:24:56 -0500 Subject: [PATCH] Minor --- theories/fp_red.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index b666bc5..b00e65c 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -881,7 +881,7 @@ Proof. Qed. Local Ltac prov_tac := sfirstorder use:depth_ren. -Local Ltac extract_tac := sfirstorder use:depth_subst_bool. +Local Ltac extract_tac := rewrite -?depth_subst_bool;hauto use:depth_subst_bool. #[tactic="prov_tac"]Equations prov {n} (A : Tm n) (B : Tm (S n)) (a : Tm n) : Prop by wf (depth_tm a) lt := prov A B (Pi A0 B0) := rtc Par.R A A0 /\ rtc Par.R B B0;