Skip to content

Commit 685c985

Browse files
aa755Yishuai Li
authored andcommitted
fixed compilation error
1 parent 5713ab9 commit 685c985

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

theories/Tactics/Forward.v

Lines changed: 1 addition & 0 deletions
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)