We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 99cf163 commit c4eacddCopy full SHA for c4eacdd
Examples/TwoPhaseCommit/TwoPhaseCoordinator.v
@@ -67,7 +67,7 @@ Next Obligation. by case/andP: H=>/eqP->_; rewrite /ddom domPt inE/=. Qed.
67
(************** Coordinator code **************)
68
69
(*** Reading internal state ***)
70
-Implicit Arguments TPCProtocol.TPCCoh [cn pts others].
+Arguments TPCProtocol.TPCCoh [cn pts others].
71
Notation coh := (@TPCProtocol.TPCCoh cn pts others).
72
Notation getS s := (getStatelet s l).
73
Notation loc i := (getLocal cn (getStatelet i l)).
0 commit comments