diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 2f496d99d8..809c502e7e 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -230,7 +230,6 @@ let rec attribute_of_vernac_command = function (* Gallina extensions *) | VernacBeginSection _ -> [] | VernacEndSegment _ -> [] - | VernacRecord _ -> [] | VernacRequire _ -> [] | VernacImport _ -> [] | VernacCanonical _ -> [] @@ -386,7 +385,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 |