diff options
| author | herbelin | 2002-11-20 21:05:43 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-20 21:05:43 +0000 |
| commit | c159424a3aa3a428676e988aa76b2bcc8c5ce646 (patch) | |
| tree | 8e6dbfea026322f7134ce8525bf6f8681745f4d9 /parsing | |
| parent | 215121fb4b8676d1b8a038c66c0690388a9e8e8c (diff) | |
Introduction d'un constructeur ARROW; rétablissement priorités des
arguments de APPTAIL (autre méthode dans g_constr.ml4 pour gérer le
conflit entre "(f 3+4)" et "(f 3!x)")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3260 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/termast.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml index bacfa24cee..698536786a 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -198,7 +198,7 @@ let rec ast_of_raw = function | RProd (_,Anonymous,t,c) -> (* Anonymous product are never factorized *) - ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)]) + ope("ARROW",[ast_of_raw t; slam(None,ast_of_raw c)]) | RLetIn (_,na,t,c) -> ope("LETIN",[ast_of_raw t; slam(idopt_of_name na,ast_of_raw c)]) |