From c6f4207c59f8e056cbd58f6e67ada6a70eaac8ad Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Jul 2002 18:13:55 +0000
Subject: Réparation d'un bug qui considérait les composantes d'un QUALID comme
 occurrences de variables indépendantes

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

diff --git a/parsing/ast.ml b/parsing/ast.ml
index e1d885a221..46fb041a7e 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -642,8 +642,10 @@ let check_typed_pat_meta env = function
 *)
 
 let rec occur_var_ast s = function
-  | Node(loc,op,args) -> List.exists (occur_var_ast s) args
+  | Node(_,"QUALID",_::_::_) -> false
+  | Node(_,"QUALID",[Nvar(_,s2)]) -> s = s2
   | Nvar(_,s2) -> s = s2
+  | Node(loc,op,args) -> List.exists (occur_var_ast s) args
   | Smetalam _ | Nmeta _ -> anomaly "occur_var: metas should not occur here"
   | Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body
   | Id _ | Str _ | Num _ | Path _ -> false
-- 
cgit v1.2.3