From 0ea28e6a440e39f9f9645aa55afbfa38a0560b27 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 13 Jan 2004 15:22:04 +0000
Subject: Reflet dans l'arbre de syntaxe de la difference syntaxique entre
 'Variables a b:A' et 'Variables (a:A) (b:A)'

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

(limited to 'ide')

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