From 84d5fa1901faba3f13a6e89c143814e2710f2f8d Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 1 Sep 2006 12:55:32 +0000
Subject: Suite commit 9110 (uniformisation position notation dans les blocs
 inductifs)

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

(limited to 'ide/coq.ml')

diff --git a/ide/coq.ml b/ide/coq.ml
index 35201ed0c..f19cd91c9 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), _, _, _) ->
-- 
cgit v1.2.3