From e32ca6edd210ccc11fb68d64af26a82354ea44aa Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 13 Jun 2003 15:29:02 +0000
Subject: CoqIDE: undo plus efficace sur les inductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4157 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/ide/coq.ml b/ide/coq.ml
index 6a21e451dd..c716699949 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -272,7 +272,8 @@ let compute_reset_info = function
   | VernacDefineModule (id, _, _, _) 
   | VernacDeclareModule (id, _, _, _)
   | VernacDeclareModuleType (id, _, _)
-  | VernacAssumption (_, (_,(id,_))::_) ->
+  | VernacAssumption (_, (_,(id,_))::_)
+  | VernacInductive (_, (id,_,_,_,_) :: _) ->
       Reset (id, ref true)
   | VernacDefinition (_, id, ProveBody _, _, _)
   | VernacStartTheoremProof (_, id, _, _, _) ->
-- 
cgit v1.2.3