Skip to content

Commit 8ab716a

Browse files
TragicusJasonGross
andauthored
Adapt to coq#19822 (#165)
* adapt to coq#19822 * Update src/Rewriter/Rewriter/ProofsCommon.v --------- Co-authored-by: Jason Gross <[email protected]>
1 parent edd0611 commit 8ab716a

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Rewriter/Rewriter/ProofsCommon.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -3674,7 +3674,7 @@ Module Compilers.
36743674
[ now eauto | intros | reflexivity ];
36753675
try solve [ fin_t ]
36763676
| progress (cbn [UnderLets.interp_related UnderLets.interp_related_gen expr.interp_related expr.interp_related_gen];
3677-
repeat (do 2 eexists; repeat apply conj; intros))
3677+
repeat (eexists; []; eexists; repeat apply conj; intros))
36783678
| solve
36793679
[ repeat
36803680
first

0 commit comments

Comments
 (0)