Skip to content

Commit

Permalink
fix coqdocjs for Set Default Proof Using commands
Browse files Browse the repository at this point in the history
  • Loading branch information
palmskog committed Jun 19, 2022
1 parent 99f4c20 commit f20ac9b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion resources/coqdocjs.js
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ function isVernacStart(l, t){
}

function isProofStart(n){
return isVernacStart(["Proof"], n.textContent) ||
return (isVernacStart(["Proof"], n.textContent) && !isVernacStart(["Using"], n.nextSibling.nextSibling.textContent)) ||
(isVernacStart(["Next"], n.textContent) && isVernacStart(["Obligation"], n.nextSibling.nextSibling.textContent));
}

Expand Down

0 comments on commit f20ac9b

Please sign in to comment.