diff options
Diffstat (limited to 'toplevel/ide_slave.ml')
| -rw-r--r-- | toplevel/ide_slave.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 9d0f17ee7..e43a23c95 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -204,7 +204,7 @@ let rec attribute_of_vernac_command = function | VernacUnfocus -> [SolveCommand] | VernacShow _ -> [OtherStatePreservingCommand] | VernacCheckGuard -> [OtherStatePreservingCommand] - | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand] + | VernacProof (None, None) -> [OtherStatePreservingCommand] | VernacProof _ -> [] | VernacProofMode _ -> [] |