Skip to content

Commit 16cdefa

Browse files
aa755liyishuai
authored andcommittedJan 4, 2024
fixed compilation error
1 parent e51a68b commit 16cdefa

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed
 

‎theories/Tactics/Forward.v

+1
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Ltac rwHyps :=
2424
| context [l] => idtac
2525
| _ => rewrite -> H
2626
end
27+
end.
2728

2829
Ltac rwHypsR :=
2930
repeat match goal with

0 commit comments

Comments
 (0)