diff options
| -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 35201ed0c4..f19cd91c9b 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -341,7 +341,7 @@ let compute_reset_info = function | VernacDeclareModule (_,(_,id), _, _) | VernacDeclareModuleType ((_,id), _, _) | VernacAssumption (_, (_,((_,id)::_,_))::_) - | VernacInductive (_, ((_,id),_,_,_,_) :: _) -> + | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> Reset (id, ref true) | VernacDefinition (_, (_,id), ProveBody _, _) | VernacStartTheoremProof (_, (_,id), _, _, _) -> |