diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-30 18:13:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-30 18:13:55 +0000 |
| commit | c6f4207c59f8e056cbd58f6e67ada6a70eaac8ad (patch) | |
| tree | 03bbb5a774b4afaa4a1e707a7d3a94b921161df3 /parsing/ast.ml | |
| parent | 2fe02b651f1977c6b9ada62c1f1457a437fa6090 (diff) | |
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
Diffstat (limited to 'parsing/ast.ml')
| -rwxr-xr-x | parsing/ast.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/ast.ml b/parsing/ast.ml index e1d885a22..46fb041a7 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 |