@@ -319,9 +319,9 @@ data Command = Quit
319 | AddProofClauseFrom Bool Int Name
319 | AddProofClauseFrom Bool Int Name
320 | AddMissing Bool Int Name
320 | AddMissing Bool Int Name
321 | MakeWith Bool Int Name
321 | MakeWith Bool Int Name
322− | DoProofSearch Bool -- ^ update
322+ | DoProofSearch Bool Bool Int Name [Name]
323− Bool -- ^ recursive (i.e. do arguments too)
323+ -- ^ the first bool is whether to update,
324− Int Name [Name]
324+ -- the second is whether to search recursively (i.e. for the arguments)
325 | SetOpt Opt
325 | SetOpt Opt
326 | UnsetOpt Opt
326 | UnsetOpt Opt
@@ -739,8 +739,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
739 | MatchRefine Name
739 | MatchRefine Name
740 | LetTac Name t | LetTacTy Name t t
740 | LetTac Name t | LetTacTy Name t t
741 | Exact t | Compute | Trivial | TCInstance
741 | 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
746 | ProofState | ProofTerm | Undo
746 | ProofState | ProofTerm | Undo