diff options
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 69d8f680f..e58a1bd19 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -375,7 +375,7 @@ let compute_reset_info = function | VernacDefinition (_, (_,id), DefineBody _, _) | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) - | VernacInductive (_, (((_,(_,id)),_,_,_,_),_) :: _) -> + | VernacInductive (_,_, (((_,(_,id)),_,_,_,_),_) :: _) -> ResetAtRegisteredObject (reset_mark id), undo_info(), ref true | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true |