@@ -319,9 +319,9 @@ data Command = Quit
319319 | AddProofClauseFrom Bool Int Name
320320 | AddMissing Bool Int Name
321321 | MakeWith Bool Int Name
322− | DoProofSearch Bool -- ^ update
323− Bool -- ^ recursive (i.e. do arguments too)
324− Int Name [Name]
322+ | DoProofSearch Bool Bool Int Name [Name]
323+ -- ^ the first bool is whether to update,
324+ -- the second is whether to search recursively (i.e. for the arguments)
325325 | SetOpt Opt
326326 | UnsetOpt Opt
327327 | NOP
@@ -739,8 +739,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
739739 | MatchRefine Name
740740 | LetTac Name t | LetTacTy Name t t
741741 | Exact t | Compute | Trivial | TCInstance
742− | ProofSearch Bool -- ^ recursive
743− (Maybe Name) [Name]
742+ | ProofSearch Bool (Maybe Name) [Name]
743+ -- ^ the bool is whether to search recursively
744744 | Solve
745745 | Attack
746746 | ProofState | ProofTerm | Undo