diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:43:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:43:05 +0000 |
| commit | f625fd3a414c3ae067e23320e382dbff5256adc4 (patch) | |
| tree | ee034269f0d3b398d2ab31d68ee67dcafac0a2a4 /parsing | |
| parent | d9c0b901668ccb2c576e7bc314c16b665311a90f (diff) | |
Prise en compte constructeur QUALID pour noms qualifiés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@865 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rwxr-xr-x | parsing/ast.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/ast.ml b/parsing/ast.ml index d154b7970..ca864ac05 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -167,7 +167,8 @@ let check_cast loc a k = [< 'sTR"cast _"; print_ast_cast k; 'sTR"failed" >]) let rec coerce_to_var v = function - | Nvar(_,id) -> id + | Nvar(_,id) -> id + | Node(_,"QUALID",[Nvar(_,id)]) -> id | ast -> user_err_loc (loc ast,"Ast.coerce_to_var", [< 'sTR"the variable "; 'sTR v; |