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 /syntax | |
| 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 'syntax')
| -rwxr-xr-x | syntax/PPConstr.v | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index d4d2ae5e63..ddc6e35638 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -82,12 +82,10 @@ Syntax constr (* Things parsed in command5 *) - level 5: - cast [ << (CAST $C $T) >> ] -> [ [<hv 0> $C:L [0 0] "::" $T:E] ] - ; (* Things parsed in command6 *) (* Things parsed in command7 *) + (* Things parsed in command8 *) level 8: lambda [ << (LAMBDA $Dom [$x]$Body) >> ] @@ -138,7 +136,7 @@ Syntax constr -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] - | arrow [ << (PROD $A [<>]$B) >> ] -> + | arrow [ << (ARROW $A [<>]$B) >> ] -> [ [<hv 0> $A:L [0 0] "->" (ARROWBOX $B) ] ] | arrow_stop [ << (ARROWBOX $c) >> ] -> [ $c:E ] | arrow_again [ << (ARROWBOX (PROD $A [<>]$B)) >> ] -> @@ -153,6 +151,9 @@ Syntax constr ; (* Things parsed in command9 *) + level 9: + cast [ << (CAST $C $T) >> ] -> [ [<hv 0> $C:L [0 0] "::" $T:E] ] + ; (* Things parsed in command10 *) level 10: @@ -175,10 +176,7 @@ Syntax constr | app_imp_last [ << (APPLISTIMPL (ACC ($LIST $A)) $T) >> ] -> [ (APPLIST ($LIST $A) $T):E ] *) - ; - (* To force parenthesis on arguments *) - level 0: | apptailcons [ << (APPTAIL $H ($LIST $T)) >> ] -> [ [1 1] $H:L (APPTAIL ($LIST $T)):E ] | apptailnil [ << (APPTAIL) >> ] -> [ ] |